1 /-
2 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro
5 -/
6 import
7 data.nat.gcd
src └──────────┘
8 data.pnat.basic data.int.sqrt data.equiv.encodable
src └─────────────┘ └───────────┘ └──────────────────┘
9 algebra.group algebra.ordered_group algebra.group_power
src └───────────┘ └───────────────────┘ └─────────────────┘
10 algebra.ordered_field
src └───────────────────┘
11 tactic.norm_cast
src └──────────────┘
12 tactic.lift
src └─────────┘
13 /-!
14 # Basics for the Rational Numbers
15
16 ## Summary
17
18 We define a rational number `q` as a structure `{ num, denom, pos, cop }`, where
19 - `num` is the numerator of `q`,
20 - `denom` is the denominator of `q`,
21 - `pos` is a proof that `denom > 0`, and
22 - `cop` is a proof `num` and `denom` are coprime.
23
24 We then define the expected (discrete) field structure on `ℚ` and prove basic lemmas about it.
25 Moreoever, we provide the expected casts from `ℕ` and `ℤ` into `ℚ`, i.e. `(↑n : ℚ) = n / 1`.
26
27 ## Main Definitions
28
29 - `rat` is the structure encoding `ℚ`.
30 - `rat.mk n d` constructs a rational number `q = n / d` from `n d : ℤ`.
31
32 ## Notations
33
34 - `/.` is infix notation for `rat.mk`.
35
36 ## Tags
37
38 rat, rationals, field, ℚ, numerator, denominator, num, denom
39 -/
40
41 /-- `rat`, or `ℚ`, is the type of rational numbers. It is defined
42 as the set of pairs ⟨n, d⟩ of integers such that `d` is positive and `n` and
43 `d` are coprime. This representation is preferred to the quotient
44 because without periodic reduction, the numerator and denominator can grow
45 exponentially (for example, adding 1/2 to itself repeatedly). -/
46 structure rat := mk' ::
47 (num : ℤ)
id ┴
src ┴
typ ┴
48 (denom : ℕ)
id ┴
src ┴
typ ┴
49 (pos : 0 < denom)
id ┴ └───┘
src ┴
typ ┴ └───┘
50 (cop : num.nat_abs.coprime denom)
id └─┘└──────┘└──────┘ └───┘
src └──────┘└──────┘
typ └─┘└──────┘└──────┘ └───┘
51 notation `ℚ` := rat
id └─┘
src └─┘
typ └─┘
doc └─┘
52
53 namespace rat
54
55 protected def repr : ℚ → string
id ┴ ┴ └────┘
src ┴ ┴ └────┘
typ ┴ ┴ └────┘
doc ┴
56 | ⟨n, d, _, _⟩ := if d = 1 then _root_.repr n else
id ┴ ┴ ┴ └─────────┘
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘
57 _root_.repr n ++ "/" ++ _root_.repr d
id └─────────┘ └┘ └┘ └─────────┘
src └─────────┘ └┘ └┘ └─────────┘
typ └─────────┘ └┘ └┘ └─────────┘
58
59 instance : has_repr ℚ := ⟨rat.repr⟩
id └──────┘ ┴ └──────┘
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ └──────┘
doc ┴
60 instance : has_to_string ℚ := ⟨rat.repr⟩
id └───────────┘ ┴ └──────┘
src └───────────┘ ┴ └──────┘
typ └───────────┘ ┴ └──────┘
doc ┴
61 meta instance : has_to_format ℚ := ⟨coe ∘ rat.repr⟩
id └───────────┘ ┴ └─┘ ┴ └──────┘
src └───────────┘ ┴ └─┘ ┴ └──────┘
typ └───────────┘ ┴ └─┘ ┴ └──────┘
doc ┴
62
63 instance : encodable ℚ := encodable.of_equiv (Σ n : ℤ, {d : ℕ // 0 < d ∧ n.nat_abs.coprime d})
id └───────┘ ┴ └────────────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘└──────┘ ┴
src └───────┘ ┴ └────────────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ └──────┘└──────┘
typ └───────┘ ┴ └────────────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘└──────┘ ┴
doc └───────┘ ┴ └────────────────┘
64 ⟨λ ⟨a, b, c, d⟩, ⟨a, b, c, d⟩, λ⟨a, b, c, d⟩, ⟨a, b, c, d⟩,
id ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
65 λ ⟨a, b, c, d⟩, rfl, λ⟨a, b, c, d⟩, rfl⟩
id ┴ └─┘ ┴ └─┘
src └─┘ └─┘
typ ┴ └─┘ ┴ └─┘
66
67 /-- Embed an integer as a rational number -/
68 def of_int (n : ℤ) : ℚ :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
69 ⟨n, 1, nat.one_pos, nat.coprime_one_right _⟩
id ┴ └─────────┘ └───────────────────┘
src └─────────┘ └───────────────────┘
typ ┴ └─────────┘ └───────────────────┘
70
71 instance : has_zero ℚ := ⟨of_int 0⟩
id └──────┘ ┴ └────┘
src └──────┘ ┴ └────┘
typ └──────┘ ┴ └────┘
doc ┴ └────┘
72 instance : has_one ℚ := ⟨of_int 1⟩
id └─────┘ ┴ └────┘
src └─────┘ ┴ └────┘
typ └─────┘ ┴ └────┘
doc ┴ └────┘
73 instance : inhabited ℚ := ⟨0⟩
id └───────┘ ┴
src └───────┘ ┴
typ └───────┘ ┴
doc ┴
74
75 /-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ+` (not necessarily coprime) -/
76 def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
id ┴ └┘ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴
doc └┘ ┴
77 let n' := n.nat_abs, g := n'.gcd d in
id └┘ ┴└──────┘ ┴ └┘└──┘
src └──────┘ └──┘
typ └┘ ┴└──────┘ ┴ └┘└──┘
78 ⟨n / g, d / g, begin
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
st └─────
79 apply (nat.le_div_iff_mul_le _ _ (nat.gcd_pos_of_pos_right _ dpos)).2,
id └───────────────────┘ └──────────────────────┘ └──┘
src └────┘ └───────────────────┘└───┘ └──────────────────────┘└─┘ └──┘
typ └────┘ └───────────────────┘└───┘ └──────────────────────┘└─┘└──┘└──┘
doc └────┘ └───┘ └─┘ └──┘
txt └────┘ └───┘ └─┘ └──┘
par └────┘ └───┘ └─┘ └──┘
pid ┴ └───┘ └─┘ └┘└┘
st ──────────────────────────────────────────────────────────────────────┘└─
80 simp, exact nat.le_of_dvd dpos (nat.gcd_dvd_right _ _)
id └───────────┘ └──┘ └───────────────┘
src └──┘ └────┘└───────────┘┴ ┴ └───────────────┘└────┘
typ └──┘ └────┘└───────────┘┴└──┘┴ └───────────────┘└────┘
doc └──┘ └────┘ ┴ ┴ └────┘
txt └──┘ └────┘ ┴ ┴ └────┘
par └──┘ └────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └───┘┴
st ─────┘└─────────────────────────────────────────────────┘
81 end, begin
st └─┘ └─────
82 have : int.nat_abs (n / ↑g) = n' / g,
id └─────────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─────┘└─────────┘┴ ┴┴┴┴ └┘┴┴ ┴ ┴
typ └─────┘└─────────┘┴ ┴┴┴┴┴ └┘┴┴└┘┴ ┴┴
doc └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
83 { cases int.nat_abs_eq n with e e; rw e, { refl },
id └────────────┘ ┴ ┴
src └────┘└────────────┘┴ └───────┘ └─┘ └───┘
typ └────┘└────────────┘┴┴└───────┘ └─┘┴ └───┘
doc └────┘ ┴ └───────┘ └─┘ └───┘
txt └────┘ ┴ └───────┘ └─┘ └───┘
par └────┘ ┴ └───────┘ └─┘ └───┘
pid ┴ ┴ └───────┘ ┴ ┴
st ───┘└──────────────────────────────────┘┴└──┘└───┘└┘└
84 rw [int.neg_div_of_dvd, int.nat_abs_neg], { refl },
id └────────────────┘ └─────────────┘
src └──┘└────────────────┘└┘└─────────────┘┴ └───┘
typ └──┘└────────────────┘└┘└─────────────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st ─────────────────────────┘└───────────────┘┴└──┘└───┘└┘└
85 exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) },
id └─────────────┘ └──────────────┘
src └────┘└─────────────┘└─┘ └──────────────┘└────┘
typ └────┘└─────────────┘└─┘ └──────────────┘└────┘
doc └────┘ └─┘ └────┘
txt └────┘ └─┘ └────┘
par └────┘ └─┘ └────┘
pid ┴ └─┘ └───┘┴
st ──────────────────────────────────────────────────┘└┘└
86 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
87 exact nat.coprime_div_gcd_div_gcd (nat.gcd_pos_of_pos_right _ dpos)
id └─────────────────────────┘ └──────────────────────┘ └──┘
src └────┘└─────────────────────────┘┴ └──────────────────────┘└─┘ └┘
typ └────┘└─────────────────────────┘┴ └──────────────────────┘└─┘└──┘└┘
doc └────┘ ┴ └─┘ └┘
txt └────┘ ┴ └─┘ └┘
par └────┘ ┴ └─┘ └┘
pid ┴ ┴ └─┘ ┴┴
st ─────────────────────────────────────────────────────────────────────┘
88 end⟩
st └─┘
89
90 /-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ`. In the case `d = 0`, we
91 define `n / 0 = 0` by convention. -/
92 def mk_nat (n : ℤ) (d : ℕ) : ℚ :=
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
doc ┴
93 if d0 : d = 0 then 0 else mk_pnat n ⟨d, nat.pos_of_ne_zero d0⟩
id └┘ ┴ ┴ └─────┘ ┴ ┴ └────────────────┘ └┘
src └┘ ┴ └─────┘ └────────────────┘
typ └┘ ┴ ┴ └─────┘ ┴ ┴ └────────────────┘ └┘
doc └─────┘
94
95 /-- Form the quotient `n / d` where `n d : ℤ`. -/
96 def mk : ℤ → ℤ → ℚ
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴
97 | n (d : ℕ) := mk_nat n d
id ┴ ┴ ┴ └────┘
src ┴ └────┘
typ ┴ ┴ ┴ └────┘
doc └────┘
98 | n -[1+ d] := mk_pnat (-n) d.succ_pnat
id ┴ └──┘ ┴┴ └─────┘ ┴ └────────┘
src └──┘ ┴ └─────┘ ┴ └────────┘
typ ┴ └──┘ ┴┴ └─────┘ ┴ └────────┘
doc └─────┘ └────────┘
99
100 localized "infix ` /. `:70 := rat.mk" in rat
101
102 theorem mk_pnat_eq (n d h) : mk_pnat n ⟨d, h⟩ = n /. d :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─────┘ ┴ └┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────┘ └┘
103 by change n /. d with dite _ _ _; simp [ne_of_gt h]
id ┴ ┴ └──┘ └──────┘ ┴
src └─────┘ ┴ ┴ └────┘└──┘└────┘ └────┘└──────┘┴ └─
typ └─────┘┴┴ ┴┴└────┘└──┘└────┘ └────┘└──────┘┴┴└─
doc └─────┘ ┴ ┴ └────┘ └────┘ └────┘ ┴ └─
txt └─────┘ ┴ ┴ └────┘ └────┘ └────┘ ┴ └─
par └─────┘ ┴ ┴ └────┘ └────┘ └────┘ ┴ └─
pid ┴ ┴ ┴ └────┘ └────┘ ┴┴ ┴ ┴└
st └─────────────────────────────────────────────────
104
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
105 theorem mk_nat_eq (n d) : mk_nat n d = n /. d := rfl
id └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src └────┘ ┴ └┘ └─┘
typ └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └────┘ └┘
106
107 @[simp] theorem mk_zero (n) : n /. 0 = 0 := rfl
id ┴ └┘ ┴ └─┘
src └┘ ┴ └─┘
typ ┴ └┘ ┴ └─┘
doc └──┘ └┘
108
109 @[simp] theorem zero_mk_pnat (n) : mk_pnat 0 n = 0 :=
id └─────┘ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴
doc └──┘ └─────┘
110 by cases n; simp [mk_pnat]; change int.nat_abs 0 with 0; simp *; refl
id ┴ └─────┘ └─────────┘
src └────┘ └────┘└─────┘┴ └─────┘└─────────┘└───────┘ └────┘ └────
typ └────┘┴ └────┘└─────┘┴ └─────┘└─────────┘└───────┘ └────┘ └────
doc └────┘ └────┘└─────┘┴ └─────┘ └───────┘ └────┘ └────
txt └────┘ └────┘ ┴ └─────┘ └───────┘ └────┘ └────
par └────┘ └────┘ ┴ └─────┘ └───────┘ └────┘ └────
pid ┴ ┴┴ ┴ ┴ ┴└─────┘┴ ┴┴ └
st └───────────────────────────────────────────────────────────────────
111
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
112 @[simp] theorem zero_mk_nat (n) : mk_nat 0 n = 0 :=
id └────┘ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴
doc └──┘ └────┘
113 by by_cases n = 0; simp [*, mk_nat]
id ┴ ┴ └────┘
src └───────┘ ┴┴└┘ └───────┘└────┘└─
typ └───────┘┴┴┴└┘ └───────┘└────┘└─
doc └───────┘ ┴ └┘ └───────┘└────┘└─
txt └───────┘ ┴ └┘ └───────┘ └─
par └───────┘ ┴ └┘ └───────┘ └─
pid ┴ ┴ ┴┴ ┴└──┘ ┴└
st └─────────────────────────────────
114
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
115 @[simp] theorem zero_mk (n) : 0 /. n = 0 :=
id └┘ ┴ ┴
src └┘ ┴
typ └┘ ┴ ┴
doc └──┘ └┘
116 by cases n; simp [mk]
id ┴ └┘
src └────┘ └────┘└┘└─
typ └────┘┴ └────┘└┘└─
doc └────┘ └────┘└┘└─
txt └────┘ └────┘ └─
par └────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └───────────────────
117
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
118 private lemma gcd_abs_dvd_left {a b} : (nat.gcd (int.nat_abs a) b : ℤ) ∣ a :=
id └─────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────────┘ ┴ ┴
typ └─────┘ └─────────┘ ┴ ┴ ┴ ┴ ┴
119 int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $ nat.gcd_dvd_left (int.nat_abs a) b
id └─────────────┘┴ └─────────────┘┴ └──────────────┘ └─────────┘ ┴ ┴
src └─────────────┘┴ └─────────────┘┴ └──────────────┘ └─────────┘
typ └─────────────┘┴ └─────────────┘┴ └──────────────┘ └─────────┘ ┴ ┴
120
121 @[simp] theorem mk_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0 :=
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘
122 begin
st └─────
123 constructor; intro h; [skip, {subst a, simp}],
id ┴ ┴
src └─────────┘ └─────┘ ┴└──┘ └────┘ └──┘
typ └─────────┘ └─────┘ ┴└──┘ └────┘┴ └──┘
doc └─────────┘ └─────┘ └──┘ └────┘ └──┘
txt └─────────┘ └─────┘ └──┘ └────┘ └──┘
par └─────────┘ └─────┘ └──┘ └────┘ └──┘
pid └┘ ┴
st ──────────────────────────────┘└──────┘└────┘└┘└─
124 have : ∀ {a b}, mk_pnat a b = 0 → a = 0,
id └─────┘ ┴
src └─────┘ └────┘ ┴└─────┘┴ ┴ ┴┴└─┘ ┴ ┴ └┘
typ └─────┘ └────┘ ┴└─────┘┴ ┴ ┴┴└─┘ ┴ ┴ └┘
doc └─────┘ └────┘ ┴└─────┘┴ ┴ ┴ └─┘ ┴ ┴ └┘
txt └─────┘ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
par └─────┘ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘
pid └───┘└┘ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ────────────────────────────────────────┘└─
125 { intros a b e, cases b with b h,
id ┴
src └──────────┘ └────┘ └───────┘
typ └──────────┘ └────┘┴└───────┘
doc └──────────┘ └────┘ └───────┘
txt └──────────┘ └────┘ └───────┘
par └──────────┘ └────┘ └───────┘
pid └────┘ ┴ └───────┘
st ───┘└──────────┘└────────────────┘└─
126 injection e with e,
id ┴
src └────────┘ └─────┘
typ └────────┘┴└─────┘
doc └────────┘ └─────┘
txt └────────┘ └─────┘
par └────────┘ └─────┘
pid ┴ └─────┘
st ─────────────────────┘└─
127 apply int.eq_mul_of_div_eq_right gcd_abs_dvd_left e },
id └────────────────────────┘ └──────────────┘ ┴
src └────┘└────────────────────────┘┴└──────────────┘┴ ┴
typ └────┘└────────────────────────┘┴└──────────────┘┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└┘└
128 cases b with b; simp [mk, mk_nat] at h,
id ┴ └┘ └────┘
src └────┘ └─────┘ └────┘└┘└┘└────┘└────┘
typ └────┘┴└─────┘ └────┘└┘└┘└────┘└────┘
doc └────┘ └─────┘ └────┘└┘└┘└────┘└────┘
txt └────┘ └─────┘ └────┘ └┘ └────┘
par └────┘ └─────┘ └────┘ └┘ └────┘
pid ┴ └─────┘ ┴┴ └┘ ┴┴└──┘
st ───────────────────────────────────────┘└─
129 { simp [mt (congr_arg int.of_nat) b0] at h,
id └┘ └───────┘ └────────┘ └┘
src └────┘└┘┴ └───────┘┴└────────┘└┘ └────┘
typ └────┘└┘┴ └───────┘┴└────────┘└┘└┘└────┘
doc └────┘ ┴ ┴ └┘ └────┘
txt └────┘ ┴ ┴ └┘ └────┘
par └────┘ ┴ ┴ └┘ └────┘
pid ┴┴ ┴ ┴ └┘ ┴┴└──┘
st ───┘└──────────────────────────────────────┘└─
130 exact this h },
id └──┘ ┴
src └────┘ ┴ ┴
typ └────┘└──┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘└┘└
131 { apply neg_inj, simp [this h] }
id └─────┘ └──┘ ┴
src └────┘└─────┘ └────┘ ┴ └┘
typ └────┘└─────┘ └────┘└──┘┴┴└┘
doc └────┘ └────┘ ┴ └┘
txt └────┘ └────┘ ┴ └┘
par └────┘ └────┘ ┴ └┘
pid ┴ ┴┴ ┴ ┴┴
st ────────────────┘└──────────────┘└─
132 end
st ──┘
133
134 theorem mk_eq : ∀ {a b c d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0),
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
135 a /. b = c /. d ↔ a * d = c * b :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘
136 suffices ∀ a b c d hb hd, mk_pnat a ⟨b, hb⟩ = mk_pnat c ⟨d, hd⟩ ↔ a * d = c * b,
id ┴ ┴ ┴ ┴ └┘ └┘ └─────┘ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ └┘ └─────┘ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
137 begin
st └─────
138 intros, cases b with b b; simp [mk, mk_nat, nat.succ_pnat],
id ┴ └┘ └────┘ └───────────┘
src └────┘ └────┘ └───────┘ └────┘└┘└┘└────┘└┘└───────────┘┴
typ └────┘ └────┘┴└───────┘ └────┘└┘└┘└────┘└┘└───────────┘┴
doc └────┘ └────┘ └───────┘ └────┘└┘└┘└────┘└┘└───────────┘┴
txt └────┘ └────┘ └───────┘ └────┘ └┘ └┘ ┴
par └────┘ └────┘ └───────┘ └────┘ └┘ └┘ ┴
pid ┴ └───────┘ ┴┴ └┘ └┘ ┴
st ───────┘└──────────────────────────────────────────────────┘└─
139 simp [mt (congr_arg int.of_nat) hb],
id └┘ └───────┘ └────────┘ └┘
src └────┘└┘┴ └───────┘┴└────────┘└┘ ┴
typ └────┘└┘┴ └───────┘┴└────────┘└┘└┘┴
doc └────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────┘└─
140 all_goals {
src └───────────
typ └───────────
doc └───────────
txt └───────────
par └───────────
pid └──
st ────────────┘└
141 cases d with d d; simp [mk, mk_nat, nat.succ_pnat],
id ┴ └┘ └────┘ └───────────┘
src ───┘└────┘ └───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘┴└─
typ ───┘└────┘┴└───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘┴└─
doc ───┘└────┘ └───────┘└┘└────┘└┘└┘└────┘└┘└───────────┘┴└─
txt ───┘└────┘ └───────┘└┘└────┘ └┘ └┘ ┴└─
par ───┘└────┘ └───────┘└┘└────┘ └┘ └┘ ┴└─
pid ─────────┘ └───────────────┘ └┘ └┘ └──
st ─────────────────────────────────────────────────────┘└─
142 simp [mt (congr_arg int.of_nat) hd],
id └┘ └───────┘ └────────┘ └┘
src ───┘└────┘└┘┴ └───────┘┴└────────┘└┘ ┴└─
typ ───┘└────┘└┘┴ └───────┘┴└────────┘└┘└┘┴└─
doc ───┘└────┘ ┴ ┴ └┘ ┴└─
txt ───┘└────┘ ┴ ┴ └┘ ┴└─
par ───┘└────┘ ┴ ┴ └┘ ┴└─
pid ─────────┘ ┴ ┴ └┘ └──
st ──────────────────────────────────────┘└─
143 all_goals { rw this, try {refl} } },
id └──┘
src ───────────────┘└─┘ └┘└───┘└──┘└┘└─┘
typ ───────────────┘└─┘└──┘└─────┘└──┘└───┘
doc ───────────────┘└─┘ └┘└───┘└──┘└┘└─┘
txt ───────────────┘└─┘ └┘└───┘└──┘└┘└─┘
par ───────────────┘└─┘ └─────┘└──┘└───┘
pid ──────────────────┘ └──────────────┘
st ──────────────┘└──────┘└─────────┘ └┘┴└┘└
144 { change a * ↑(d.succ) = -c * ↑b ↔ a * -(d.succ) = c * b,
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └─────┘ ┴┴┴┴ └┘┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└┘ ┴ ┴ ┴
typ └─────┘ ┴┴┴┴ └┘┴┴┴ ┴ ┴ ┴ ┴┴┴ ┴ └────┘└┘ ┴┴┴ ┴┴
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───┘└────────────────────────────────────────────────────┘└─
145 constructor; intro h; apply neg_inj; simpa [left_distrib, neg_add_eq_iff_eq_add,
id └─────┘ └──────────┘ └───────────────────┘
src └─────────┘ └─────┘ └────┘└─────┘ └─────┘└──────────┘└┘└───────────────────┘└─
typ └─────────┘ └─────┘ └────┘└─────┘ └─────┘└──────────┘└┘└───────────────────┘└─
doc └─────────┘ └─────┘ └────┘ └─────┘ └┘ └─
txt └─────────┘ └─────┘ └────┘ └─────┘ └┘ └─
par └─────────┘ └─────┘ └────┘ └─────┘ └┘ └─
pid └┘ ┴ ┴┴ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────
146 eq_neg_iff_add_eq_zero, neg_eq_iff_add_eq_zero] using h },
id └────────────────────┘ └────────────────────┘ ┴
src ─────┘└────────────────────┘└┘└────────────────────┘└──────┘ ┴
typ ─────┘└────────────────────┘└┘└────────────────────┘└──────┘┴┴
doc ─────┘ └┘ └──────┘ ┴
txt ─────┘ └┘ └──────┘ ┴
par ─────┘ └┘ └──────┘ ┴
pid ─────┘ └┘ ┴┴└────┘ ┴
st ─────────────────────────────────────────────────────────────┘└┘└
147 { change -a * ↑d = c * b.succ ↔ a * d = c * -b.succ,
id ┴ ┴ ┴ └────┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴┴┴ ┴ └────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───┘└───────────────────────────────────────────────┘└─
148 constructor; intro h; apply neg_inj; simpa [left_distrib, eq_comm] using h },
id └─────┘ └──────────┘ └─────┘ ┴
src └─────────┘ └─────┘ └────┘└─────┘ └─────┘└──────────┘└┘└─────┘└──────┘ ┴
typ └─────────┘ └─────┘ └────┘└─────┘ └─────┘└──────────┘└┘└─────┘└──────┘┴┴
doc └─────────┘ └─────┘ └────┘ └─────┘ └┘ └──────┘ ┴
txt └─────────┘ └─────┘ └────┘ └─────┘ └┘ └──────┘ ┴
par └─────────┘ └─────┘ └────┘ └─────┘ └┘ └──────┘ ┴
pid └┘ ┴ ┴┴ └┘ ┴┴└────┘ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└┘└
149 { change -a * d.succ = -c * b.succ ↔ a * -d.succ = c * -b.succ,
id ┴ └────┘ ┴ └────┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ ┴ └────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └────┘┴ ┴┴┴ ┴ └────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└─
150 simp [left_distrib] }
id └──────────┘
src └────┘└──────────┘└┘
typ └────┘└──────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────────────────────┘└─
151 end,
st ──┘
152 begin
st └─────
153 intros, simp [mk_pnat], constructor; intro h,
id └─────┘
src └────┘ └────┘└─────┘┴ └─────────┘ └─────┘
typ └────┘ └────┘└─────┘┴ └─────────┘ └─────┘
doc └────┘ └────┘└─────┘┴ └─────────┘ └─────┘
txt └────┘ └────┘ ┴ └─────────┘ └─────┘
par └────┘ └────┘ ┴ └─────────┘ └─────┘
pid ┴┴ ┴ └┘
st ───────┘└──────────────┘└────────────────────┘└─
154 { cases h with ha hb,
id ┴
src └────┘ └─────────┘
typ └────┘┴└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ───┘└────────────────┘└─
155 have ha, {
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └─────┘
st ──────────┘└──┘
156 have dv := @gcd_abs_dvd_left,
id └──────────────┘
src └─────────┘ └──────────────┘
typ └─────────┘ └──────────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────┘┴└─┘
st └────────────────────────────────┘└─
157 have := int.eq_mul_of_div_eq_right dv ha,
id └────────────────────────┘ └┘ └┘
src └──────┘└────────────────────────┘┴ ┴
typ └──────┘└────────────────────────┘┴└┘┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
158 rw ← int.mul_div_assoc _ dv at this,
id └───────────────┘ └┘
src └───┘└───────────────┘└─┘ └──────┘
typ └───┘└───────────────┘└─┘└┘└──────┘
doc └───┘ └─┘ └──────┘
txt └───┘ └─┘ └──────┘
par └───┘ └─┘ └──────┘
pid └─┘ └─┘ └──────┘
st ────────────────────────────────────────┘└─
159 exact int.eq_mul_of_div_eq_left (dvd_mul_of_dvd_right dv _) this.symm },
id └───────────────────────┘ └──────────────────┘ └┘ └───────┘
src └────┘└───────────────────────┘┴ └──────────────────┘┴ └──┘└───────┘┴
typ └────┘└───────────────────────┘┴ └──────────────────┘┴└┘└──┘└───────┘┴
doc └────┘ ┴ ┴ └──┘ ┴
txt └────┘ ┴ ┴ └──┘ ┴
par └────┘ ┴ ┴ └──┘ ┴
pid ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────┘└┘└
160 have hb, {
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └─────┘
st ──────────┘└──┘
161 have dv := λ {a b}, nat.gcd_dvd_right (int.nat_abs a) b,
id └───────────────┘ └─────────┘
src └─────────┘ └──────┘└───────────────┘┴ └─────────┘┴ └┘
typ └─────────┘ └──────┘└───────────────┘┴ └─────────┘┴ └┘
doc └─────────┘ └──────┘ ┴ ┴ └┘
txt └─────────┘ └──────┘ ┴ ┴ └┘
par └─────────┘ └──────┘ ┴ ┴ └┘
pid └─────┘┴└─┘ └──────┘ ┴ ┴ └┘
st └───────────────────────────────────────────────────────────┘└─
162 have := nat.eq_mul_of_div_eq_right dv hb,
id └────────────────────────┘ └┘ └┘
src └──────┘└────────────────────────┘┴ ┴
typ └──────┘└────────────────────────┘┴└┘┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
163 rw ← nat.mul_div_assoc _ dv at this,
id └───────────────┘ └┘
src └───┘└───────────────┘└─┘ └──────┘
typ └───┘└───────────────┘└─┘└┘└──────┘
doc └───┘ └─┘ └──────┘
txt └───┘ └─┘ └──────┘
par └───┘ └─┘ └──────┘
pid └─┘ └─┘ └──────┘
st ────────────────────────────────────────┘└─
164 exact nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_right dv _) this.symm },
id └───────────────────────┘ └──────────────────┘ └┘ └───────┘
src └────┘└───────────────────────┘┴ └──────────────────┘┴ └──┘└───────┘┴
typ └────┘└───────────────────────┘┴ └──────────────────┘┴└┘└──┘└───────┘┴
doc └────┘ ┴ ┴ └──┘ ┴
txt └────┘ ┴ ┴ └──┘ ┴
par └────┘ ┴ ┴ └──┘ ┴
pid ┴ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────┘└┘└
165 have m0 : (a.nat_abs.gcd b * c.nat_abs.gcd d : ℤ) ≠ 0, {
id └───────────┘ ┴ └───────────┘ ┴ ┴
src └────────┘ └───────────┘┴ ┴ ┴└───────────┘┴ └─┘ └┘┴└┘
typ └────────┘ └───────────┘┴┴┴ ┴└───────────┘┴┴└─┘ └┘┴└┘
doc └────────┘ ┴ ┴ ┴ ┴ └─┘ └┘ └┘
txt └────────┘ ┴ ┴ ┴ ┴ └─┘ └┘ └┘
par └────────┘ ┴ ┴ ┴ ┴ └─┘ └┘ └┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴┴
st ────────────────────────────────────────────────────────┘└──┘
166 refine int.coe_nat_ne_zero.2 (ne_of_gt _),
id └─────────────────┘ └──────┘
src └─────┘└─────────────────┘└─┘ └──────┘└─┘
typ └─────┘└─────────────────┘└─┘ └──────┘└─┘
doc └─────┘ └─┘ └─┘
txt └─────┘ └─┘ └─┘
par └─────┘ └─┘ └─┘
pid ┴ └─┘ └─┘
st └─────────────────────────────────────────────┘└─
167 apply mul_pos; apply nat.gcd_pos_of_pos_right; assumption },
id └─────┘ └──────────────────────┘
src └────┘└─────┘ └────┘└──────────────────────┘ └─────────┘
typ └────┘└─────┘ └────┘└──────────────────────┘ └─────────┘
doc └────┘ └────┘ └─────────┘
txt └────┘ └────┘ └─────────┘
par └────┘ └────┘ └─────────┘
pid ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────┘└┘└
168 apply eq_of_mul_eq_mul_right m0,
id └────────────────────┘ └┘
src └────┘└────────────────────┘┴
typ └────┘└────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└─
169 simpa [mul_comm, mul_left_comm] using
id └──────┘ └───────────┘
src └─────┘└──────┘└┘└───────────┘└───────
typ └─────┘└──────┘└┘└───────────┘└───────
doc └─────┘ └┘ └───────
txt └─────┘ └┘ └───────
par └─────┘ └┘ └───────
pid ┴┴ └┘ ┴┴└─────
st ──────────────────────────────────────────
170 congr (congr_arg (*) ha.symm) (congr_arg coe hb) },
id └───┘ ┴ └─────┘ └───────┘ └─┘ └┘
src ─────┘└───┘┴ ┴┴└─┘└─────┘└┘ └───────┘┴└─┘┴ └┘
typ ─────┘└───┘┴ ┴┴└─┘└─────┘└┘ └───────┘┴└─┘┴└┘└┘
doc ─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘
txt ─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘
par ─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘
pid ─────┘ ┴ ┴ └─┘ └┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────┘└┘└
171 { suffices : ∀ a c, a * d = c * b →
id ┴
src └─────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
typ └─────────┘ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └
doc └─────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
txt └─────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └─────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └───────┘└┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ──────────────────────────────────────
172 a / a.gcd b = c / c.gcd d ∧ b / a.gcd b = d / c.gcd d,
id ┴ └──┘ └──┘ ┴ ┴
src ─────┘ ┴┴┴ └──┘┴ ┴ ┴ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ─────┘ ┴┴┴ └──┘┴ ┴ ┴ ┴ ┴ └──┘┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
173 { cases this a.nat_abs c.nat_abs
id └──┘ └───────┘ └───────┘
src └────┘ ┴└───────┘┴└───────┘└
typ └────┘└──┘┴└───────┘┴└───────┘└
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────┘└──────────────────────────────
174 (by simpa [int.nat_abs_mul] using congr_arg int.nat_abs h) with h₁ h₂,
id └─────────────┘ └───────┘ └─────────┘ ┴
src ───────┘ ┴└─────┘└─────────────┘└──────┘└───────┘┴└─────────┘┴ └──────────┘
typ ───────┘ ┴└─────┘└─────────────┘└──────┘└───────┘┴└─────────┘┴┴└──────────┘
doc ───────┘ ┴└─────┘ └──────┘ ┴ ┴ └──────────┘
txt ───────┘ ┴└─────┘ └──────┘ ┴ ┴ └──────────┘
par ───────┘ ┴└─────┘ └──────┘ ┴ ┴ └──────────┘
pid ───────┘ └──────┘ └──────┘ ┴ ┴ ┴└─────────┘
st ──────────┘└────────────────────────────────────────────────────┘└──────────┘└─
175 have hs := congr_arg int.sign h,
id └───────┘ └──────┘ ┴
src └─────────┘└───────┘┴└──────┘┴
typ └─────────┘└───────┘┴└──────┘┴┴
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────────────────────┘└─
176 simp [int.sign_eq_one_of_pos (int.coe_nat_lt.2 hb),
id └────────────────────┘ └────────────┘ └┘
src └────┘└────────────────────┘┴ └────────────┘└─┘ └──
typ └────┘└────────────────────┘┴ └────────────┘└─┘└┘└──
doc └────┘ ┴ └─┘ └──
txt └────┘ ┴ └─┘ └──
par └────┘ ┴ └─┘ └──
pid ┴┴ ┴ └─┘ └──
st ──────────────────────────────────────────────────────────
177 int.sign_eq_one_of_pos (int.coe_nat_lt.2 hd)] at hs,
id └────────────────────┘ └────────────┘ └┘
src ───────────┘└────────────────────┘┴ └────────────┘└─┘ └──────┘
typ ───────────┘└────────────────────┘┴ └────────────┘└─┘└┘└──────┘
doc ───────────┘ ┴ └─┘ └──────┘
txt ───────────┘ ┴ └─┘ └──────┘
par ───────────┘ ┴ └─┘ └──────┘
pid ───────────┘ ┴ └─┘ └┘┴└───┘
st ──────────────────────────────────────────────────────────────┘└─
178 conv in a { rw ← int.sign_mul_nat_abs a },
id ┴ └──────────────────┘ ┴
src └──────┘ └─┘└───┘└──────────────────┘┴ ┴┴
typ └──────┘┴└─┘└───┘└──────────────────┘┴┴┴┴
txt └──────┘ └─┘└───┘ ┴ ┴┴
par └──────┘ └─┘└───┘ ┴ ┴┴
pid ┴└─┘ └──────┘ ┴ └┘
st ────────────────┘└───────────────────────────┘└┘└
179 conv in c { rw ← int.sign_mul_nat_abs c },
id ┴ └──────────────────┘ ┴
src └──────┘ └─┘└───┘└──────────────────┘┴ ┴┴
typ └──────┘┴└─┘└───┘└──────────────────┘┴┴┴┴
txt └──────┘ └─┘└───┘ ┴ ┴┴
par └──────┘ └─┘└───┘ ┴ ┴┴
pid ┴└─┘ └──────┘ ┴ └┘
st ────────────────┘└───────────────────────────┘└┘└
180 rw [int.mul_div_assoc, int.mul_div_assoc],
id └───────────────┘ └───────────────┘
src └──┘└───────────────┘└┘└───────────────┘┴
typ └──┘└───────────────┘└┘└───────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────┘└─────────────────┘└──
181 exact ⟨congr (congr_arg (*) hs) (congr_arg coe h₁), h₂⟩,
id └───┘ └┘ └───────┘ └─┘ └┘ └┘
src └────┘ └───┘┴ ┴ └─┘ └┘ └───────┘┴└─┘┴ └─┘ ┴
typ └────┘ └───┘┴ ┴ └─┘└┘└┘ └───────┘┴└─┘┴└┘└─┘└┘┴
doc └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴
txt └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴
par └────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴
pid ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴
st ────────────────────────────────────────────────────────────┘└─
182 all_goals { exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) } },
id └─────────────┘ └──────────────┘
src └──────────┘└────┘└─────────────┘└─┘ └──────────────┘└────┘└┘
typ └──────────┘└────┘└─────────────┘└─┘ └──────────────┘└────┘└┘
doc └──────────┘└────┘ └─┘ └────┘└┘
txt └──────────┘└────┘ └─┘ └────┘└┘
par └──────────┘└────┘ └─┘ └────┘└┘
pid └───────┘ └─┘ └─────┘┴
st ────────────────┘└──────────────────────────────────────────────┘┴┴└┘└
183 intros a c h,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ───────────────┘└─
184 suffices bd : b / a.gcd b = d / c.gcd d,
id └───┘ ┴ └───┘ ┴
src └────────────┘ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴└───┘┴
typ └────────────┘ ┴ ┴└───┘┴┴┴ ┴ ┴ ┴└───┘┴┴
doc └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
185 { refine ⟨_, bd⟩,
id └┘
src └─────┘ └─┘ ┴
typ └─────┘ └─┘└┘┴
doc └─────┘ └─┘ ┴
txt └─────┘ └─┘ ┴
par └─────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────┘└────────────┘└─
186 apply nat.eq_of_mul_eq_mul_left hb,
id └───────────────────────┘ └┘
src └────┘└───────────────────────┘┴
typ └────┘└───────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────┘└─
187 rw [← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _), mul_comm,
id └───────────────┘ └──────────────┘ └──────┘
src └────┘└───────────────┘└─┘ └──────────────┘└─────┘└──────┘└─
typ └────┘└───────────────┘└─┘ └──────────────┘└─────┘└──────┘└─
doc └────┘ └─┘ └─────┘ └─
txt └────┘ └─┘ └─────┘ └─
par └────┘ └─┘ └─────┘ └─
pid └──┘ └─┘ └─────┘ └─
st ─────────────────────────────────────────────────────┘└────────┘└─
188 nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), bd,
id └───────────────┘ └───────────────┘ └┘
src ─────────┘└───────────────┘└─┘ └───────────────┘└─────┘ └─
typ ─────────┘└───────────────┘└─┘ └───────────────┘└─────┘└┘└─
doc ─────────┘ └─┘ └─────┘ └─
txt ─────────┘ └─┘ └─────┘ └─
par ─────────┘ └─┘ └─────┘ └─
pid ─────────┘ └─┘ └─────┘ └─
st ────────────────────────────────────────────────────┘└──┘└─
189 ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), h, mul_comm,
id └───────────────┘ └───────────────┘ ┴ └──────┘
src ───────────┘└───────────────┘└─┘ └───────────────┘└─────┘ └┘└──────┘└─
typ ───────────┘└───────────────┘└─┘ └───────────────┘└─────┘┴└┘└──────┘└─
doc ───────────┘ └─┘ └─────┘ └┘ └─
txt ───────────┘ └─┘ └─────┘ └┘ └─
par ───────────┘ └─┘ └─────┘ └┘ └─
pid ───────────┘ └─┘ └─────┘ └┘ └─
st ──────────────────────────────────────────────────────┘└─┘└────────┘└─
190 nat.mul_div_assoc _ (nat.gcd_dvd_left _ _)] },
id └───────────────┘ └──────────────┘
src ─────────┘└───────────────┘└─┘ └──────────────┘└─────┘
typ ─────────┘└───────────────┘└─┘ └──────────────┘└─────┘
doc ─────────┘ └─┘ └─────┘
txt ─────────┘ └─┘ └─────┘
par ─────────┘ └─┘ └─────┘
pid ─────────┘ └─┘ └────┘┴
st ───────────────────────────────────────────────────┘┴┴└┘└
191 suffices : ∀ {a c : ℕ} (b>0) (d>0),
src └─────────┘ └──────┘ └───────────┘ └
typ └─────────┘ └──────┘ └───────────┘ └
doc └─────────┘ └──────┘ └───────────┘ └
txt └─────────┘ └──────┘ └───────────┘ └
par └─────────┘ └──────┘ └───────────┘ └
pid └───────┘└┘ └──────┘ └───────────┘ └
st ────────────────────────────────────────
192 a * d = c * b → b / a.gcd b ≤ d / c.gcd d,
id ┴ └──┘ ┴ └──┘
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘┴ ┴┴┴ ┴ ┴ └──┘┴
typ ─────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘┴ ┴┴┴ ┴ ┴ └──┘┴
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
193 { exact le_antisymm (this _ hb _ hd h) (this _ hd _ hb h.symm) },
id └─────────┘ └──┘ └┘ └┘ └────┘
src └────┘└─────────┘┴ └─┘ └─┘ ┴ └┘ └─┘ └─┘ ┴└────┘└┘
typ └────┘└─────────┘┴ └─┘ └─┘ ┴ └┘ └──┘└─┘└┘└─┘└┘┴└────┘└┘
doc └────┘ ┴ └─┘ └─┘ ┴ └┘ └─┘ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ └─┘ ┴ └┘ └─┘ └─┘ ┴ └┘
par └────┘ ┴ └─┘ └─┘ ┴ └┘ └─┘ └─┘ ┴ └┘
pid ┴ ┴ └─┘ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴┴
st ─────┘└───────────────────────────────────────────────────────────┘└┘└
194 intros a c b hb d hd h,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ─────────────────────────┘└─
195 have gb0 := nat.gcd_pos_of_pos_right a hb,
id └──────────────────────┘ ┴ └┘
src └──────────┘└──────────────────────┘┴ ┴
typ └──────────┘└──────────────────────┘┴┴┴└┘
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴
st ────────────────────────────────────────────┘└─
196 have gd0 := nat.gcd_pos_of_pos_right c hd,
id └──────────────────────┘ ┴ └┘
src └──────────┘└──────────────────────┘┴ ┴
typ └──────────┘└──────────────────────┘┴┴┴└┘
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid └──────┘┴└─┘ ┴ ┴
st ────────────────────────────────────────────┘└─
197 apply nat.le_of_dvd,
id └───────────┘
src └────┘└───────────┘
typ └────┘└───────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────┘└─
198 apply (nat.le_div_iff_mul_le _ _ gd0).2,
id └───────────────────┘ └─┘
src └────┘ └───────────────────┘└───┘ └─┘
typ └────┘ └───────────────────┘└───┘└─┘└─┘
doc └────┘ └───┘ └─┘
txt └────┘ └───┘ └─┘
par └────┘ └───┘ └─┘
pid ┴ └───┘ ┴└┘
st ──────────────────────────────────────────┘└─
199 simp, apply nat.le_of_dvd hd (nat.gcd_dvd_right _ _),
id └───────────┘ └┘ └───────────────┘
src └──┘ └────┘└───────────┘┴ ┴ └───────────────┘└───┘
typ └──┘ └────┘└───────────┘┴└┘┴ └───────────────┘└───┘
doc └──┘ └────┘ ┴ ┴ └───┘
txt └──┘ └────┘ ┴ ┴ └───┘
par └──┘ └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ └───┘
st ───────┘└──────────────────────────────────────────────┘└─
200 apply (nat.coprime_div_gcd_div_gcd gb0).symm.dvd_of_dvd_mul_left,
id └─────────────────────────┘ └─┘
src └────┘ └─────────────────────────┘┴ └────────────────────────┘
typ └────┘ └─────────────────────────┘┴└─┘└────────────────────────┘
doc └────┘ ┴ └────────────────────────┘
txt └────┘ ┴ └────────────────────────┘
par └────┘ ┴ └────────────────────────┘
pid ┴ ┴ └───────────────────────┘┴
st ───────────────────────────────────────────────────────────────────┘└─
201 refine ⟨c / c.gcd d, _⟩,
id └───┘ ┴
src └─────┘ ┴ ┴└───┘┴ └──┘
typ └─────┘ ┴ ┴└───┘┴┴└──┘
doc └─────┘ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ └──┘
st ──────────────────────────┘└─
202 rw [← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _),
id └───────────────┘ └──────────────┘
src └────┘└───────────────┘└─┘ └──────────────┘└──────
typ └────┘└───────────────┘└─┘ └──────────────┘└──────
doc └────┘ └─┘ └──────
txt └────┘ └─┘ └──────
par └────┘ └─┘ └──────
pid └──┘ └─┘ └──────
st ───────────────────────────────────────────────────┘└─
203 ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _)],
id └───────────────┘ └───────────────┘
src ─────────┘└───────────────┘└─┘ └───────────────┘└────┘
typ ─────────┘└───────────────┘└─┘ └───────────────┘└────┘
doc ─────────┘ └─┘ └────┘
txt ─────────┘ └─┘ └────┘
par ─────────┘ └─┘ └────┘
pid ─────────┘ └─┘ └────┘
st ────────────────────────────────────────────────────┘└──
204 apply congr_arg (/ c.gcd d),
id └───────┘ ┴ └───┘ ┴
src └────┘└───────┘┴┴└┘└───┘┴ ┴
typ └────┘└───────┘┴┴└┘└───┘┴┴┴
doc └────┘ ┴ └┘ ┴ ┴
txt └────┘ ┴ └┘ ┴ ┴
par └────┘ ┴ └┘ ┴ ┴
pid ┴ ┴ └┘ ┴ ┴
st ──────────────────────────────┘└─
205 rw [mul_comm, ← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _),
id └──────┘ └───────────────┘ └──────────────┘
src └──┘└──────┘└──┘└───────────────┘└─┘ └──────────────┘└──────
typ └──┘└──────┘└──┘└───────────────┘└─┘ └──────────────┘└──────
doc └──┘ └──┘ └─┘ └──────
txt └──┘ └──┘ └─┘ └──────
par └──┘ └──┘ └─┘ └──────
pid └┘ └──┘ └─┘ └──────
st ───────────────┘└────────────────────────────────────────────┘└─
206 mul_comm, h, nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), mul_comm] }
id └──────┘ ┴ └───────────────┘ └───────────────┘ └──────┘
src ───────┘└──────┘└┘ └┘└───────────────┘└─┘ └───────────────┘└─────┘└──────┘└┘
typ ───────┘└──────┘└┘┴└┘└───────────────┘└─┘ └───────────────┘└─────┘└──────┘└┘
doc ───────┘ └┘ └┘ └─┘ └─────┘ └┘
txt ───────┘ └┘ └┘ └─┘ └─────┘ └┘
par ───────┘ └┘ └┘ └─┘ └─────┘ └┘
pid ───────┘ └┘ └┘ └─┘ └─────┘ ┴┴
st ───────────────┘└─┘└───────────────────────────────────────────┘└────────┘┴┴└─
207 end
st ──┘
208
209 @[simp] theorem div_mk_div_cancel_left {a b c : ℤ} (c0 : c ≠ 0) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc └──┘
210 (a * c) /. (b * c) = a /. b :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘ └┘
211 begin
st └─────
212 by_cases b0 : b = 0, { subst b0, simp },
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴└┘ └────┘ └───┘
typ └───────┘ └─┘┴┴┴└┘ └────┘└┘ └───┘
doc └───────┘ └─┘ ┴ └┘ └────┘ └───┘
txt └───────┘ └─┘ ┴ └┘ └────┘ └───┘
par └───────┘ └─┘ ┴ └┘ └────┘ └───┘
pid ┴ └─┘ ┴ ┴┴ ┴ ┴
st ────────────────────┘└──┘└──────┘└─────┘└┘└
213 apply (mk_eq (mul_ne_zero b0 c0) b0).2, simp [mul_comm, mul_assoc]
id └───┘ └─────────┘ └┘ └┘ └──────┘ └───────┘
src └────┘ └───┘┴ └─────────┘┴ ┴ └┘ └─┘ └────┘└──────┘└┘└───────┘└┘
typ └────┘ └───┘┴ └─────────┘┴ ┴└┘└┘└┘└─┘ └────┘└──────┘└┘└───────┘└┘
doc └────┘ ┴ ┴ ┴ └┘ └─┘ └────┘ └┘ └┘
txt └────┘ ┴ ┴ ┴ └┘ └─┘ └────┘ └┘ └┘
par └────┘ ┴ ┴ ┴ └┘ └─┘ └────┘ └┘ └┘
pid ┴ ┴ ┴ ┴ └┘ ┴└┘ ┴┴ └┘ ┴┴
st ───────────────────────────────────────┘└───────────────────────────┘
214 end
st └─┘
215
216 @[simp] theorem num_denom : ∀ {a : ℚ}, a.num /. a.denom = a
id ┴ ┴ ┴└──┘ └┘ ┴└────┘ ┴ ┴
src ┴ └──┘ └┘ └────┘ ┴
typ ┴ ┴ ┴└──┘ └┘ ┴└────┘ ┴ ┴
doc └──┘ ┴ └┘
217 | ⟨n, d, h, (c:_=1)⟩ := show mk_nat n d = _,
id ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘ ┴
typ ┴ ┴ ┴ └────┘ ┴
doc └────┘
218 by simp [mk_nat, ne_of_gt h, mk_pnat, c]
id └────┘ └──────┘ ┴ └─────┘ ┴
src └────┘└────┘└┘└──────┘┴ └┘└─────┘└┘ └─
typ └────┘└────┘└┘└──────┘┴┴└┘└─────┘└┘┴└─
doc └────┘└────┘└┘ ┴ └┘└─────┘└┘ └─
txt └────┘ └┘ ┴ └┘ └┘ └─
par └────┘ └┘ ┴ └┘ └┘ └─
pid ┴┴ └┘ ┴ └┘ └┘ ┴└
st └──────────────────────────────────────
219
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
220 theorem num_denom' {n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d := num_denom.symm
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘└───┘
src ┴ ┴ └┘ └───────┘└───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘└───┘
doc ┴ └┘
221
222 theorem of_int_eq_mk (z : ℤ) : of_int z = z /. 1 := num_denom'
id ┴ └────┘ ┴ ┴ ┴ └┘ └────────┘
src ┴ └────┘ ┴ └┘ └────────┘
typ ┴ └────┘ ┴ ┴ ┴ └┘ └────────┘
doc └────┘ └┘
223
224 @[elab_as_eliminator] def {u} num_denom_cases_on {C : ℚ → Sort u}
id ┴
src ┴
typ ┴
doc └────────────────┘ ┴
225 : ∀ (a : ℚ) (H : ∀ n d, 0 < d → (int.nat_abs n).coprime d → C (n /. d)), C a
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ └─────────┘ └─────┘ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc ┴ └┘
226 | ⟨n, d, h, c⟩ H := by rw num_denom'; exact H n d h c
id └────────┘ ┴ ┴ ┴ ┴ ┴
src └─┘└────────┘ └────┘ ┴ ┴ ┴ ┴ └
typ └─┘└────────┘ └────┘┴┴┴┴┴┴┴┴┴└
doc └─┘ └────┘ ┴ ┴ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ ┴ └
st └───────────────────────────────
227
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
228 @[elab_as_eliminator] def {u} num_denom_cases_on' {C : ℚ → Sort u}
id ┴
src ┴
typ ┴
doc └────────────────┘ ┴
229 (a : ℚ) (H : ∀ (n:ℤ) (d:ℕ), d ≠ 0 → C (n /. d)) : C a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc ┴ └┘
230 num_denom_cases_on a $ λ n d h c,
id └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴
231 H n d $ ne_of_gt h
id ┴ ┴ ┴ └──────┘ ┴
src └──────┘
typ ┴ ┴ ┴ └──────┘ ┴
232
233 theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a :=
id ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴
src ┴ ┴ └┘ └─┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴
doc └┘
234 begin
st └─────
235 cases e : a /. b with n d h c,
id ┴ ┴
src └────┘ └─┘ ┴ ┴ └───────────┘
typ └────┘ └─┘┴┴ ┴┴└───────────┘
doc └────┘ └─┘ ┴ ┴ └───────────┘
txt └────┘ └─┘ ┴ ┴ └───────────┘
par └────┘ └─┘ ┴ ┴ └───────────┘
pid ┴ └─┘ ┴ ┴ └───────────┘
st ──────────────────────────────┘└─
236 rw [rat.num_denom', rat.mk_eq b0
id └────────────┘ └───────┘ └┘
src └──┘└────────────┘└┘└───────┘┴ └
typ └──┘└────────────┘└┘└───────┘┴└┘└
doc └──┘ └┘ ┴ └
txt └──┘ └┘ ┴ └
par └──┘ └┘ ┴ └
pid └┘ └┘ ┴ └
st ───────────────────┘└──────────────
237 (ne_of_gt (int.coe_nat_pos.2 h))] at e,
id └──────┘ └─────────────┘ ┴
src ───┘ └──────┘┴ └─────────────┘└─┘ └──────┘
typ ───┘ └──────┘┴ └─────────────┘└─┘┴└──────┘
doc ───┘ ┴ └─┘ └──────┘
txt ───┘ ┴ └─┘ └──────┘
par ───┘ ┴ └─┘ └──────┘
pid ───┘ ┴ └─┘ └─┘└───┘
st ───────────────────────────────────┘┴└───┘└─
238 refine (int.nat_abs_dvd.1 $ int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $
id └─────────────┘ └─────────────┘ └─────────────┘
src └─────┘ └─────────────┘└─┘ ┴└─────────────┘└─┘ ┴└─────────────┘└─┘ └
typ └─────┘ └─────────────┘└─┘ ┴└─────────────┘└─┘ ┴└─────────────┘└─┘ └
doc └─────┘ └─┘ ┴ └─┘ ┴ └─┘ └
txt └─────┘ └─┘ ┴ └─┘ ┴ └─┘ └
par └─────┘ └─┘ ┴ └─┘ ┴ └─┘ └
pid ┴ └─┘ ┴ └─┘ ┴ └─┘ └
st ──────────────────────────────────────────────────────────────────────
239 c.dvd_of_dvd_mul_right _),
id └────────────────────┘
src ───┘└────────────────────┘└─┘
typ ───┘└────────────────────┘└─┘
doc ───┘ └─┘
txt ───┘ └─┘
par ───┘ └─┘
pid ───┘ └─┘
st ────────────────────────────┘└─
240 have := congr_arg int.nat_abs e,
id └───────┘ └─────────┘ ┴
src └──────┘└───────┘┴└─────────┘┴
typ └──────┘└───────┘┴└─────────┘┴┴
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ────────────────────────────────┘└─
241 simp [int.nat_abs_mul, int.nat_abs_of_nat] at this, simp [this]
id └─────────────┘ └────────────────┘ └──┘
src └────┘└─────────────┘└┘└────────────────┘└───────┘ └────┘ └┘
typ └────┘└─────────────┘└┘└────────────────┘└───────┘ └────┘└──┘└┘
doc └────┘ └┘ └───────┘ └────┘ └┘
txt └────┘ └┘ └───────┘ └────┘ └┘
par └────┘ └┘ └───────┘ └────┘ └┘
pid ┴┴ └┘ ┴┴└─────┘ ┴┴ ┴┴
st ───────────────────────────────────────────────────┘└────────────┘
242 end
st └─┘
243
244 theorem denom_dvd (a b : ℤ) : ((a /. b).denom : ℤ) ∣ b :=
id ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴
src ┴ └┘ └───┘ ┴ ┴
typ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴
doc └┘
245 begin
st └─────
246 by_cases b0 : b = 0, {simp [b0]},
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴└┘ └────┘ ┴
typ └───────┘ └─┘┴┴┴└┘ └────┘└┘┴
doc └───────┘ └─┘ ┴ └┘ └────┘ ┴
txt └───────┘ └─┘ ┴ └┘ └────┘ ┴
par └───────┘ └─┘ ┴ └┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴┴ ┴┴ ┴
st ────────────────────┘└──────────┘└┘└
247 cases e : a /. b with n d h c,
id ┴ ┴
src └────┘ └─┘ ┴ ┴ └───────────┘
typ └────┘ └─┘┴┴ ┴┴└───────────┘
doc └────┘ └─┘ ┴ ┴ └───────────┘
txt └────┘ └─┘ ┴ ┴ └───────────┘
par └────┘ └─┘ ┴ ┴ └───────────┘
pid ┴ └─┘ ┴ ┴ └───────────┘
st ──────────────────────────────┘└─
248 rw [num_denom', mk_eq b0 (ne_of_gt (int.coe_nat_pos.2 h))] at e,
id └────────┘ └───┘ └┘ └──────┘ └─────────────┘ ┴
src └──┘└────────┘└┘└───┘┴ ┴ └──────┘┴ └─────────────┘└─┘ └──────┘
typ └──┘└────────┘└┘└───┘┴└┘┴ └──────┘┴ └─────────────┘└─┘┴└──────┘
doc └──┘ └┘ ┴ ┴ ┴ └─┘ └──────┘
txt └──┘ └┘ ┴ ┴ ┴ └─┘ └──────┘
par └──┘ └┘ ┴ ┴ ┴ └─┘ └──────┘
pid └┘ └┘ ┴ ┴ ┴ └─┘ └─┘└───┘
st ───────────────┘└─────────────────────────────────────────┘┴└───┘└─
249 refine (int.dvd_nat_abs.1 $ int.coe_nat_dvd.2 $ c.symm.dvd_of_dvd_mul_left _),
id └─────────────┘ └─────────────┘ └────────────────────────┘
src └─────┘ └─────────────┘└─┘ ┴└─────────────┘└─┘ ┴└────────────────────────┘└─┘
typ └─────┘ └─────────────┘└─┘ ┴└─────────────┘└─┘ ┴└────────────────────────┘└─┘
doc └─────┘ └─┘ ┴ └─┘ ┴ └─┘
txt └─────┘ └─┘ ┴ └─┘ ┴ └─┘
par └─────┘ └─┘ ┴ └─┘ ┴ └─┘
pid ┴ └─┘ ┴ └─┘ ┴ └─┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
250 rw [← int.nat_abs_mul, ← int.coe_nat_dvd, int.dvd_nat_abs, ← e], simp
id └─────────────┘ └─────────────┘ └─────────────┘ ┴
src └────┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘└──┘ ┴ └───┘
typ └────┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘└──┘┴┴ └───┘
doc └────┘ └──┘ └┘ └──┘ ┴ └───┘
txt └────┘ └──┘ └┘ └──┘ ┴ └───┘
par └────┘ └──┘ └┘ └──┘ ┴ └───┘
pid └──┘ └──┘ └┘ └──┘ ┴ ┴
st ──────────────────────┘└─────────────────┘└───────────────┘└───┘└──────┘
251 end
st └─┘
252
253 protected def add : ℚ → ℚ → ℚ
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
254 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * d₂ + n₂ * d₁) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
id └┘ └┘ └┘ └┘ └┘ └┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘
src └─────┘ ┴ ┴ ┴ ┴ └─────┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └─────┘ ┴ ┴ ┴ ┴ └─────┘
doc └─────┘
255
256 instance : has_add ℚ := ⟨rat.add⟩
id └─────┘ ┴ └─────┘
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ └─────┘
doc ┴
257
258 theorem lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
259 (fv : ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂},
id └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
260 f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = f₁ n₁ d₁ n₂ d₂ /. f₂ n₁ d₁ n₂ d₂)
id ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src ┴ └┘
typ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
doc └┘
261 (f0 : ∀ {n₁ d₁ n₂ d₂} (d₁0 : d₁ ≠ 0) (d₂0 : d₂ ≠ 0), f₂ n₁ d₁ n₂ d₂ ≠ 0)
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴
src ┴ ┴ ┴
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴
262 (a b c d : ℤ) (b0 : b ≠ 0) (d0 : d ≠ 0)
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
263 (H : ∀ {n₁ d₁ n₂ d₂} (h₁ : a * d₁ = n₁ * b) (h₂ : c * d₂ = n₂ * d),
id └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
264 f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
id └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘
src ┴ ┴ ┴
typ └┘ └┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘
265 f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ ┴ └┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘
266 begin
st └─────
267 generalize ha : a /. b = x, cases x with n₁ d₁ h₁ c₁, rw num_denom' at ha,
id ┴ ┴ ┴ └────────┘
src └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘└────────┘└────┘
typ └──────────────┘┴┴ ┴┴┴ ┴ └────┘┴└───────────────┘ └─┘└────────┘└────┘
doc └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
txt └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
par └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
pid └─┘└┘┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ └────┘
st ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
268 generalize hc : c /. d = x, cases x with n₂ d₂ h₂ c₂, rw num_denom' at hc,
id ┴ ┴ ┴ └────────┘
src └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘└────────┘└────┘
typ └──────────────┘┴┴ ┴┴┴ ┴ └────┘┴└───────────────┘ └─┘└────────┘└────┘
doc └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
txt └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
par └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
pid └─┘└┘┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ └────┘
st ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
269 rw fv,
src └─┘
typ └─┘└┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────┘└─
270 have d₁0 := ne_of_gt (int.coe_nat_lt.2 h₁),
id └──────┘ └────────────┘ └┘
src └──────────┘└──────┘┴ └────────────┘└─┘ ┴
typ └──────────┘└──────┘┴ └────────────┘└─┘└┘┴
doc └──────────┘ ┴ └─┘ ┴
txt └──────────┘ ┴ └─┘ ┴
par └──────────┘ ┴ └─┘ ┴
pid └──────┘┴└─┘ ┴ └─┘ ┴
st ───────────────────────────────────────────┘└─
271 have d₂0 := ne_of_gt (int.coe_nat_lt.2 h₂),
id └──────┘ └────────────┘ └┘
src └──────────┘└──────┘┴ └────────────┘└─┘ ┴
typ └──────────┘└──────┘┴ └────────────┘└─┘└┘┴
doc └──────────┘ ┴ └─┘ ┴
txt └──────────┘ ┴ └─┘ ┴
par └──────────┘ ┴ └─┘ ┴
pid └──────┘┴└─┘ ┴ └─┘ ┴
st ───────────────────────────────────────────┘└─
272 exact (mk_eq (f0 d₁0 d₂0) (f0 b0 d0)).2 (H ((mk_eq b0 d₁0).1 ha) ((mk_eq d0 d₂0).1 hc))
id └┘ ┴ └┘ └─┘ └┘ └───┘ └┘ └─┘ └┘
src └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └┘ └───┘┴ ┴ └──┘ └─┘
typ └────┘ ┴ ┴ ┴ └┘ └┘┴ ┴ └───┘ ┴┴ ┴└┘┴└─┘└──┘└┘└┘ └───┘┴└┘┴└─┘└──┘└┘└─┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ └─┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ └─┘
par └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ └─┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ └┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘
273 end
st └─┘
274
275 @[simp] theorem add_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
276 a /. b + c /. d = (a * d + c * b) /. (b * d) :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
277 begin
st └─────
278 apply lift_binop_eq rat.add; intros; try {assumption},
id └───────────┘ └─────┘
src └────┘└───────────┘┴└─────┘ └────┘ └───┘└────────┘┴
typ └────┘└───────────┘┴└─────┘ └────┘ └───┘└────────┘┴
doc └────┘ ┴ └────┘ └───┘└────────┘┴
txt └────┘ ┴ └────┘ └───┘└────────┘┴
par └────┘ ┴ └────┘ └───┘└────────┘┴
pid ┴ ┴ └───────────┘
st ───────────────────────────────────────────┘└────────┘└┘└
279 { apply mk_pnat_eq },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└───────────────┘└┘└
280 { apply mul_ne_zero d₁0 d₂0 },
id └─────────┘ └─┘ └─┘
src └────┘└─────────┘┴ ┴ ┴
typ └────┘└─────────┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└────────────────────────┘└┘└
281 calc (n₁ * d₂ + n₂ * d₁) * (b * d) =
id └──┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴
doc └──┘
st ───────────────────────────────────────
282 (n₁ * b) * d₂ * d + (n₂ * d) * (d₁ * b) : by simp [mul_add, mul_comm, mul_left_comm]
id └┘ └┘ └┘ ┴ └┘ ┴ └─────┘ └──────┘ └───────────┘
src └────┘└─────┘└┘└──────┘└┘└───────────┘└─
typ └┘ └┘ └┘ ┴ └┘ ┴ └────┘└─────┘└┘└──────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st ─────────────────────────────────────────────────────┘└────────────────────────────────────────
283 ... = (a * d₁) * d₂ * d + (c * d₂) * (d₁ * b) : by rw [h₁, h₂]
id └┘ └┘
src ───┘ └──┘ └┘ └─
typ ───┘ └──┘└┘└┘└┘└─
doc ───┘ └──┘ └┘ └─
txt ───┘ └──┘ └┘ └─
par ───┘ └──┘ └┘ └─
pid ───┘ └┘ └┘ ┴└
st ───┘└────────────────────────────────────────────────┘└─────┘└──┘┴└
284 ... = (a * d + c * b) * (d₁ * d₂) : by simp [mul_add, mul_comm, mul_left_comm]
id ┴ ┴ └─────┘ └──────┘ └───────────┘
src ───┘ └────┘└─────┘└┘└──────┘└┘└───────────┘└┘
typ ───┘ ┴ ┴ └────┘└─────┘└┘└──────┘└┘└───────────┘└┘
doc ───┘ └────┘ └┘ └┘ └┘
txt ───┘ └────┘ └┘ └┘ └┘
par ───┘ └────┘ └┘ └┘ └┘
pid ───┘ ┴┴ └┘ └┘ ┴┴
st ───┘└────────────────────────────────────────────────┘└───────────────────────────────────────┘
285 end
st └─┘
286
287 protected def neg : ℚ → ℚ
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc ┴ ┴
288 | ⟨n, d, h, c⟩ := ⟨-n, d, h, by simp [c]⟩
id ┴ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴
typ ┴ ┴ ┴ ┴ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
289
290 instance : has_neg ℚ := ⟨rat.neg⟩
id └─────┘ ┴ └─────┘
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ └─────┘
doc ┴
291
292 @[simp] theorem neg_def {a b : ℤ} : -(a /. b) = -a /. b :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └┘ ┴
src ┴ ┴ └┘ ┴ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └┘ ┴
doc └──┘ └┘ └┘
293 begin
st └─────
294 by_cases b0 : b = 0, { subst b0, simp, refl },
id ┴ ┴ └┘
src └───────┘ └──┘ ┴┴└┘ └────┘ └──┘ └───┘
typ └───────┘ └──┘┴┴┴└┘ └────┘└┘ └──┘ └───┘
doc └───────┘ └──┘ ┴ └┘ └────┘ └──┘ └───┘
txt └───────┘ └──┘ ┴ └┘ └────┘ └──┘ └───┘
par └───────┘ └──┘ ┴ └┘ └────┘ └──┘ └───┘
pid ┴ └──┘ ┴ ┴┴ ┴ ┴
st ─────────────────────┘└──┘└──────┘└────┘└─────┘└┘└
295 generalize ha : a /. b = x, cases x with n₁ d₁ h₁ c₁, rw num_denom' at ha,
id ┴ ┴ ┴ └────────┘
src └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘└────────┘└────┘
typ └──────────────┘┴┴ ┴┴┴ ┴ └────┘┴└───────────────┘ └─┘└────────┘└────┘
doc └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
txt └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
par └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────────┘ └─┘ └────┘
pid └─┘└┘┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ └────┘
st ───────────────────────────┘└────────────────────────┘└───────────────────┘└─
296 show rat.mk' _ _ _ _ = _, rw num_denom',
id └─────┘ └────────┘
src └───┘└─────┘└───────┘ └┘ └─┘└────────┘
typ └───┘└─────┘└───────┘ └┘ └─┘└────────┘
doc └───┘ └───────┘ └┘ └─┘
txt └───┘ └───────┘ └┘ └─┘
par └───┘ └───────┘ └┘ └─┘
pid └───┘ └───────┘ └┘ ┴
st ─────────────────────────┘└─────────────┘└─
297 have d0 := ne_of_gt (int.coe_nat_lt.2 h₁),
id └──────┘ └────────────┘ └┘
src └─────────┘└──────┘┴ └────────────┘└─┘ ┴
typ └─────────┘└──────┘┴ └────────────┘└─┘└┘┴
doc └─────────┘ ┴ └─┘ ┴
txt └─────────┘ ┴ └─┘ ┴
par └─────────┘ ┴ └─┘ ┴
pid └─────┘┴└─┘ ┴ └─┘ ┴
st ──────────────────────────────────────────┘└─
298 apply (mk_eq d0 b0).2, have h₁ := (mk_eq b0 d0).1 ha,
id └───┘ └┘ └┘ └───┘ └┘ └┘ └┘
src └────┘ └───┘┴ ┴ └─┘ └─────────┘ └───┘┴ ┴ └──┘
typ └────┘ └───┘┴└┘┴└┘└─┘ └─────────┘ └───┘┴└┘┴└┘└──┘└┘
doc └────┘ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └──┘
txt └────┘ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └──┘
par └────┘ ┴ ┴ └─┘ └─────────┘ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴└┘ └─────┘┴└─┘ ┴ ┴ └──┘
st ──────────────────────┘└─────────────────────────────┘└─
299 simp only [neg_mul_eq_neg_mul_symm, congr_arg has_neg.neg h₁]
id └─────────────────────┘ └───────┘ └─────────┘ └┘
src └─────────┘└─────────────────────┘└┘└───────┘┴└─────────┘┴ └┘
typ └─────────┘└─────────────────────┘└┘└───────┘┴└─────────┘┴└┘└┘
doc └─────────┘ └┘ ┴ ┴ └┘
txt └─────────┘ └┘ ┴ ┴ └┘
par └─────────┘ └┘ ┴ ┴ └┘
pid ┴└──┘└┘ └┘ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────────────────┘
300 end
st └─┘
301
302 protected def mul : ℚ → ℚ → ℚ
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
303 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * n₂) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
id └┘ └┘ └┘ └┘ └┘ └┘ └─────┘ ┴ ┴ └─────┘
src └─────┘ ┴ ┴ └─────┘
typ └┘ └┘ └┘ └┘ └┘ └┘ └─────┘ ┴ ┴ └─────┘
doc └─────┘
304
305 instance : has_mul ℚ := ⟨rat.mul⟩
id └─────┘ ┴ └─────┘
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ └─────┘
doc ┴
306
307 @[simp] theorem mul_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
308 (a /. b) * (c /. d) = (a * c) /. (b * d) :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
309 begin
st └─────
310 apply lift_binop_eq rat.mul; intros; try {assumption},
id └───────────┘ └─────┘
src └────┘└───────────┘┴└─────┘ └────┘ └───┘└────────┘┴
typ └────┘└───────────┘┴└─────┘ └────┘ └───┘└────────┘┴
doc └────┘ ┴ └────┘ └───┘└────────┘┴
txt └────┘ ┴ └────┘ └───┘└────────┘┴
par └────┘ ┴ └────┘ └───┘└────────┘┴
pid ┴ ┴ └───────────┘
st ───────────────────────────────────────────┘└────────┘└┘└
311 { apply mk_pnat_eq },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└───────────────┘└┘└
312 { apply mul_ne_zero d₁0 d₂0 },
id └─────────┘ └─┘ └─┘
src └────┘└─────────┘┴ ┴ ┴
typ └────┘└─────────┘┴└─┘┴└─┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└────────────────────────┘└┘└
313 cc
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────┘
314 end
st └─┘
315
316 protected def inv : ℚ → ℚ
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
doc ┴ ┴
317 | ⟨(n+1:ℕ), d, h, c⟩ := ⟨d, n+1, n.succ_pos, c.symm⟩
id ┴┴ ┴ ┴ ┴ ┴ └───────┘ └───┘
src ┴ ┴ ┴ └───────┘ └───┘
typ ┴┴ ┴ ┴ ┴ ┴ └───────┘ └───┘
318 | ⟨0, d, h, c⟩ := 0
319 | ⟨-[1+ n], d, h, c⟩ := ⟨-d, n+1, n.succ_pos, nat.coprime.symm $ by simp; exact c⟩
id └──┘ ┴┴ ┴ ┴ ┴ └───────┘ └──────────────┘ ┴
src └──┘ ┴ ┴ ┴ └───────┘ └──────────────┘ └──┘ └────┘
typ └──┘ ┴┴ ┴ ┴ ┴ └───────┘ └──────────────┘ └──┘ └────┘┴
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴
st └────────────┘
320
321 instance : has_inv ℚ := ⟨rat.inv⟩
id └─────┘ ┴ └─────┘
src └─────┘ ┴ └─────┘
typ └─────┘ ┴ └─────┘
doc ┴
322
323 @[simp] theorem inv_def {a b : ℤ} : (a /. b)⁻¹ = b /. a :=
id ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ └┘
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └┘ └┘
324 begin
st └─────
325 by_cases a0 : a = 0, { subst a0, simp, refl },
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴└┘ └────┘ └──┘ └───┘
typ └───────┘ └─┘┴┴┴└┘ └────┘└┘ └──┘ └───┘
doc └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
txt └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
par └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
pid ┴ └─┘ ┴ ┴┴ ┴ ┴
st ────────────────────┘└──┘└──────┘└────┘└─────┘└┘└
326 by_cases b0 : b = 0, { subst b0, simp, refl },
id ┴ └┘
src └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
typ └───────┘ └─┘┴┴ └┘ └────┘└┘ └──┘ └───┘
doc └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
txt └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
par └───────┘ └─┘ ┴ └┘ └────┘ └──┘ └───┘
pid ┴ └─┘ ┴ ┴┴ ┴ ┴
st ────────────────────┘└──┘└──────┘└────┘└─────┘└┘└
327 generalize ha : a /. b = x, cases x with n d h c, rw num_denom' at ha,
id ┴ ┴ ┴ └────────┘
src └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────┘ └─┘└────────┘└────┘
typ └──────────────┘┴┴ ┴┴┴ ┴ └────┘┴└───────────┘ └─┘└────────┘└────┘
doc └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────┘ └─┘ └────┘
txt └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────┘ └─┘ └────┘
par └──────────────┘ ┴ ┴ ┴ ┴ └────┘ └───────────┘ └─┘ └────┘
pid └─┘└┘┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └────┘
st ───────────────────────────┘└────────────────────┘└───────────────────┘└─
328 refine eq.trans (_ : rat.inv ⟨n, d, h, c⟩ = d /. n) _,
id └──────┘ └─────┘ ┴ ┴ ┴ ┴
src └─────┘└──────┘┴ └──┘└─────┘┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘
typ └─────┘└──────┘┴ └──┘└─────┘┴ └┘ └┘┴└┘┴└┘ ┴┴┴ ┴┴└─┘
doc └─────┘ ┴ └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘
txt └─────┘ ┴ └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘
par └─────┘ ┴ └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────┘└─
329 { cases n with n; [cases n with n, skip],
id ┴ ┴ ┴
src └────┘ └─────┘ ┴└────┘ └─────┘ └──┘
typ └────┘┴└─────┘ ┴└────┘┴└─────┘ └──┘
doc └────┘ └─────┘ └────┘ └─────┘ └──┘
txt └────┘ └─────┘ └────┘ └─────┘ └──┘
par └────┘ └─────┘ └────┘ └─────┘ └──┘
pid ┴ └─────┘ ┴ └─────┘
st ───┘└────────────────────────────────────┘└─
330 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────┘└───┘└┘└
331 { change int.of_nat n.succ with (n+1:ℕ),
id └────────┘ └────┘ ┴┴
src └─────┘└────────┘┴└────┘└────┘ ┴└┘ ┴
typ └─────┘└────────┘┴└────┘└────┘ ┴┴└┘ ┴
doc └─────┘ ┴ └────┘ └┘ ┴
txt └─────┘ ┴ └────┘ └┘ ┴
par └─────┘ ┴ └────┘ └┘ ┴
pid ┴ ┴ └────┘ └┘ ┴
st ─────┘└───────────────────────────────────┘└─
332 unfold rat.inv, rw num_denom' },
id └────────┘
src └────────────┘ └─┘└────────┘┴
typ └────────────┘ └─┘└────────┘┴
doc └────────────┘ └─┘ ┴
txt └────────────┘ └─┘ ┴
par └────────────┘ └─┘ ┴
pid └──────┘ ┴ ┴
st ───────────────────┘└──────────────┘└┘└
333 { unfold rat.inv, rw num_denom', refl } },
id └────────┘
src └────────────┘ └─┘└────────┘ └───┘
typ └────────────┘ └─┘└────────┘ └───┘
doc └────────────┘ └─┘ └───┘
txt └────────────┘ └─┘ └───┘
par └────────────┘ └─┘ └───┘
pid └──────┘ ┴ ┴
st ───────────────────┘└─────────────┘└─────┘└──┘└
334 have n0 : n ≠ 0,
id ┴ ┴
src └────────┘ ┴┴└┘
typ └────────┘┴┴┴└┘
doc └────────┘ ┴ └┘
txt └────────┘ ┴ └┘
par └────────┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴┴
st ────────────────┘└─
335 { refine mt (λ (n0 : n = 0), _) a0,
id └┘ ┴ ┴ └┘
src └─────┘└┘┴ └─────┘ ┴ └──────┘
typ └─────┘└┘┴ └─────┘┴┴┴└──────┘└┘
doc └─────┘ ┴ └─────┘ ┴ └──────┘
txt └─────┘ ┴ └─────┘ ┴ └──────┘
par └─────┘ ┴ └─────┘ ┴ └──────┘
pid ┴ ┴ └─────┘ ┴ └──────┘
st ───┘└──────────────────────────────┘└─
336 subst n0, simp at ha,
id └┘
src └────┘ └────────┘
typ └────┘└┘ └────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ ┴└───┘
st ───────────┘└──────────┘└─
337 exact (mk_eq_zero b0).1 ha },
id └────────┘ └┘ └┘
src └────┘ └────────┘┴ └──┘ ┴
typ └────┘ └────────┘┴└┘└──┘└┘┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ──────────────────────────────┘└┘└
338 have d0 := ne_of_gt (int.coe_nat_lt.2 h),
id └──────┘ └────────────┘ ┴
src └─────────┘└──────┘┴ └────────────┘└─┘ ┴
typ └─────────┘└──────┘┴ └────────────┘└─┘┴┴
doc └─────────┘ ┴ └─┘ ┴
txt └─────────┘ ┴ └─┘ ┴
par └─────────┘ ┴ └─┘ ┴
pid └─────┘┴└─┘ ┴ └─┘ ┴
st ─────────────────────────────────────────┘└─
339 have ha := (mk_eq b0 d0).1 ha,
id └───┘ └┘ └┘ └┘
src └─────────┘ └───┘┴ ┴ └──┘
typ └─────────┘ └───┘┴└┘┴└┘└──┘└┘
doc └─────────┘ ┴ ┴ └──┘
txt └─────────┘ ┴ ┴ └──┘
par └─────────┘ ┴ ┴ └──┘
pid └─────┘┴└─┘ ┴ ┴ └──┘
st ──────────────────────────────┘└─
340 apply (mk_eq n0 a0).2,
id └───┘ └┘ └┘
src └────┘ └───┘┴ ┴ └─┘
typ └────┘ └───┘┴└┘┴└┘└─┘
doc └────┘ ┴ ┴ └─┘
txt └────┘ ┴ ┴ └─┘
par └────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴└┘
st ──────────────────────┘└─
341 cc
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────┘
342 end
st └─┘
343
344 variables (a b c : ℚ)
id ┴
src ┴
typ ┴
doc ┴
345
346 protected theorem add_zero : a + 0 = a :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
347 num_denom_cases_on' a $ λ n d h,
id └─────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴
348 by rw [← zero_mk d]; simp [h, -zero_mk]
id └─────┘ ┴ ┴
src └────┘└─────┘┴ ┴ └────┘ └───────────
typ └────┘└─────┘┴┴┴ └────┘┴└───────────
doc └────┘ ┴ ┴ └────┘ └───────────
txt └────┘ ┴ ┴ └────┘ └───────────
par └────┘ ┴ ┴ └────┘ └───────────
pid └──┘ ┴ ┴ ┴┴ └─────────┘└
st └──────────────┘┴└────────────────────
349
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
350 protected theorem zero_add : 0 + a = a :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
351 num_denom_cases_on' a $ λ n d h,
id └─────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴
352 by rw [← zero_mk d]; simp [h, -zero_mk]
id └─────┘ ┴ ┴
src └────┘└─────┘┴ ┴ └────┘ └───────────
typ └────┘└─────┘┴┴┴ └────┘┴└───────────
doc └────┘ ┴ ┴ └────┘ └───────────
txt └────┘ ┴ ┴ └────┘ └───────────
par └────┘ ┴ ┴ └────┘ └───────────
pid └──┘ ┴ ┴ ┴┴ └─────────┘└
st └──────────────┘┴└────────────────────
353
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
354 protected theorem add_comm : a + b = b + a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
355 num_denom_cases_on' a $ λ n₁ d₁ h₁,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
356 num_denom_cases_on' b $ λ n₂ d₂ h₂,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
357 by simp [h₁, h₂, mul_comm]
id └┘ └┘ └──────┘
src └────┘ └┘ └┘└──────┘└─
typ └────┘└┘└┘└┘└┘└──────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └────────────────────────
358
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
359 protected theorem add_assoc : a + b + c = a + (b + c) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
360 num_denom_cases_on' a $ λ n₁ d₁ h₁,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
361 num_denom_cases_on' b $ λ n₂ d₂ h₂,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
362 num_denom_cases_on' c $ λ n₃ d₃ h₃,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
363 by simp [h₁, h₂, h₃, mul_ne_zero, mul_add, mul_comm, mul_left_comm, add_left_comm]
id └┘ └┘ └┘ └─────────┘ └─────┘ └──────┘ └───────────┘ └───────────┘
src └────┘ └┘ └┘ └┘└─────────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└───────────┘└─
typ └────┘└┘└┘└┘└┘└┘└┘└─────────┘└┘└─────┘└┘└──────┘└┘└───────────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
364
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
365 protected theorem add_left_neg : -a + a = 0 :=
id ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴
366 num_denom_cases_on' a $ λ n d h,
id └─────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴
367 by simp [h]
id ┴
src └────┘ └─
typ └────┘┴└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 protected theorem mul_one : a * 1 = a :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
370 num_denom_cases_on' a $ λ n d h,
id └─────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴
371 by change (1:ℚ) with 1 /. 1; simp [h]
id └┘ ┴
src └─────┘ └┘ └───────┘└┘└┘ └────┘ └─
typ └─────┘ └┘ └───────┘└┘└┘ └────┘┴└─
doc └─────┘ └┘ └───────┘└┘└┘ └────┘ └─
txt └─────┘ └┘ └───────┘ └┘ └────┘ └─
par └─────┘ └┘ └───────┘ └┘ └────┘ └─
pid ┴ └┘ ┴└──────┘ ┴┴ ┴┴ ┴└
st └───────────────────────────────────
372
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
373 protected theorem one_mul : 1 * a = a :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
374 num_denom_cases_on' a $ λ n d h,
id └─────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴
375 by change (1:ℚ) with 1 /. 1; simp [h]
id └┘ ┴
src └─────┘ └┘ └───────┘└┘└┘ └────┘ └─
typ └─────┘ └┘ └───────┘└┘└┘ └────┘┴└─
doc └─────┘ └┘ └───────┘└┘└┘ └────┘ └─
txt └─────┘ └┘ └───────┘ └┘ └────┘ └─
par └─────┘ └┘ └───────┘ └┘ └────┘ └─
pid ┴ └┘ ┴└──────┘ ┴┴ ┴┴ ┴└
st └───────────────────────────────────
376
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
377 protected theorem mul_comm : a * b = b * a :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
378 num_denom_cases_on' a $ λ n₁ d₁ h₁,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
379 num_denom_cases_on' b $ λ n₂ d₂ h₂,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
380 by simp [h₁, h₂, mul_comm]
id └┘ └┘ └──────┘
src └────┘ └┘ └┘└──────┘└─
typ └────┘└┘└┘└┘└┘└──────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └────────────────────────
381
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
382 protected theorem mul_assoc : a * b * c = a * (b * c) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
383 num_denom_cases_on' a $ λ n₁ d₁ h₁,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
384 num_denom_cases_on' b $ λ n₂ d₂ h₂,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
385 num_denom_cases_on' c $ λ n₃ d₃ h₃,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
386 by simp [h₁, h₂, h₃, mul_ne_zero, mul_comm, mul_left_comm]
id └┘ └┘ └┘ └─────────┘ └──────┘ └───────────┘
src └────┘ └┘ └┘ └┘└─────────┘└┘└──────┘└┘└───────────┘└─
typ └────┘└┘└┘└┘└┘└┘└┘└─────────┘└┘└──────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────
387
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
388 protected theorem add_mul : (a + b) * c = a * c + b * c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
389 num_denom_cases_on' a $ λ n₁ d₁ h₁,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
390 num_denom_cases_on' b $ λ n₂ d₂ h₂,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
391 num_denom_cases_on' c $ λ n₃ d₃ h₃,
id └─────────────────┘ ┴ └┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ └┘ └┘ └┘
392 by simp [h₁, h₂, h₃, mul_ne_zero];
id └┘ └┘ └┘ └─────────┘
src └────┘ └┘ └┘ └┘└─────────┘┴
typ └────┘└┘└┘└┘└┘└┘└┘└─────────┘┴
doc └────┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ └┘ ┴
st └────────────────────────────────
393 refine (div_mk_div_cancel_left (int.coe_nat_ne_zero.2 h₃)).symm.trans _;
id └────────────────────┘ └─────────────────┘ └┘
src └─────┘ └────────────────────┘┴ └─────────────────┘└─┘ └─────────────┘
typ └─────┘ └────────────────────┘┴ └─────────────────┘└─┘└┘└─────────────┘
doc └─────┘ ┴ └─┘ └─────────────┘
txt └─────┘ ┴ └─┘ └─────────────┘
par └─────┘ ┴ └─┘ └─────────────┘
pid ┴ ┴ └─┘ └─────────────┘
st ────────────────────────────────────────────────────────────────────────────
394 simp [mul_add, mul_comm, mul_assoc, mul_left_comm]
id └─────┘ └──────┘ └───────┘ └───────────┘
src └────┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
typ └────┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ ┴└
st ──────────────────────────────────────────────────────
395
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
396 protected theorem mul_add : a * (b + c) = a * b + a * c :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
397 by rw [rat.mul_comm, rat.add_mul, rat.mul_comm, rat.mul_comm c a]
id └──────────┘ └─────────┘ └──────────┘ └──────────┘ ┴ ┴
src └──┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────────┘┴ ┴ └─
typ └──┘└──────────┘└┘└─────────┘└┘└──────────┘└┘└──────────┘┴┴┴┴└─
doc └──┘ └┘ └┘ └┘ ┴ ┴ └─
txt └──┘ └┘ └┘ └┘ ┴ ┴ └─
par └──┘ └┘ └┘ └┘ ┴ ┴ └─
pid └┘ └┘ └┘ └┘ ┴ ┴ ┴└
st └───────────────┘└───────────┘└────────────┘└────────────────┘┴└
398
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
399 protected theorem zero_ne_one : 0 ≠ (1:ℚ) :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
400 mt (λ (h : 0 = 1 /. 1), (mk_eq_zero one_ne_zero).1 h.symm) one_ne_zero
id └┘ ┴ └┘ └────────┘ └─────────┘ ┴ ┴└───┘ └─────────┘
src └┘ ┴ └┘ └────────┘ └─────────┘ ┴ └───┘ └─────────┘
typ └┘ ┴ └┘ └────────┘ └─────────┘ ┴ ┴└───┘ └─────────┘
doc └┘
401
402 protected theorem mul_inv_cancel : a ≠ 0 → a * a⁻¹ = 1 :=
id ┴ ┴ ┴ ┴ ┴└┘ ┴
src ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴└┘ ┴
403 num_denom_cases_on' a $ λ n d h a0,
id └─────────────────┘ ┴ ┴ ┴ ┴ └┘
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴ ┴ └┘
404 have n0 : n ≠ 0, from mt (by intro e; subst e; simp) a0,
id ┴ ┴ └┘ ┴ └┘
src ┴ └┘ └─────┘ └────┘ └──┘
typ ┴ ┴ └┘ └─────┘ └────┘┴ └──┘ └┘
doc └─────┘ └────┘ └──┘
txt └─────┘ └────┘ └──┘
par └─────┘ └────┘ └──┘
pid └┘ ┴
st └─────────────────────┘
405 by simp [h, n0, mul_comm]; exact
id ┴ └┘ └──────┘
src └────┘ └┘ └┘└──────┘┴ └────┘
typ └────┘┴└┘└┘└┘└──────┘┴ └────┘
doc └────┘ └┘ └┘ ┴ └────┘
txt └────┘ └┘ └┘ ┴ └────┘
par └────┘ └┘ └┘ ┴ └────┘
pid ┴┴ └┘ └┘ ┴ ┴
st └──────────────────────────────
406 eq.trans (by simp) (@div_mk_div_cancel_left 1 1 _ n0)
id └──────┘ └────────────────────┘ └┘
src └──────┘┴ ┴└──┘└┘ └────────────────────┘└─────┘ └─
typ └──────┘┴ ┴└──┘└┘ └────────────────────┘└─────┘└┘└─
doc ┴ ┴└──┘└┘ └─────┘ └─
txt ┴ ┴└──┘└┘ └─────┘ └─
par ┴ ┴└──┘└┘ └─────┘ └─
pid ┴ └─────┘ └─────┘ ┴└
st ───────────┘└───┘└────────────────────────────────────
407
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
408 protected theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
id ┴ ┴ ┴└┘ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ ┴└┘ ┴ ┴ ┴
409 eq.trans (rat.mul_comm _ _) (rat.mul_inv_cancel _ h)
id └──────┘ └──────────┘ └────────────────┘ ┴
src └──────┘ └──────────┘ └────────────────┘
typ └──────┘ └──────────┘ └────────────────┘ ┴
410
411 instance : decidable_eq ℚ := by tactic.mk_dec_eq_instance
id └──────────┘ ┴ └───────────────────────┘
src └──────────┘ ┴ └───────────────────────┘
typ └──────────┘ ┴ └───────────────────────┘
doc ┴
par └───────────────────────┘
st └────────────────────────┘
412
413 instance : discrete_field ℚ :=
id └────────────┘ ┴
src └────────────┘ ┴
typ └────────────┘ ┴
doc ┴
414 { zero := 0,
415 add := rat.add,
id └─────┘
src └─────┘
typ └─────┘
416 neg := rat.neg,
id └─────┘
src └─────┘
typ └─────┘
417 one := 1,
418 mul := rat.mul,
id └─────┘
src └─────┘
typ └─────┘
419 inv := rat.inv,
id └─────┘
src └─────┘
typ └─────┘
420 zero_add := rat.zero_add,
id └──────────┘
src └──────────┘
typ └──────────┘
421 add_zero := rat.add_zero,
id └──────────┘
src └──────────┘
typ └──────────┘
422 add_comm := rat.add_comm,
id └──────────┘
src └──────────┘
typ └──────────┘
423 add_assoc := rat.add_assoc,
id └───────────┘
src └───────────┘
typ └───────────┘
424 add_left_neg := rat.add_left_neg,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
425 mul_one := rat.mul_one,
id └─────────┘
src └─────────┘
typ └─────────┘
426 one_mul := rat.one_mul,
id └─────────┘
src └─────────┘
typ └─────────┘
427 mul_comm := rat.mul_comm,
id └──────────┘
src └──────────┘
typ └──────────┘
428 mul_assoc := rat.mul_assoc,
id └───────────┘
src └───────────┘
typ └───────────┘
429 left_distrib := rat.mul_add,
id └─────────┘
src └─────────┘
typ └─────────┘
430 right_distrib := rat.add_mul,
id └─────────┘
src └─────────┘
typ └─────────┘
431 zero_ne_one := rat.zero_ne_one,
id └─────────────┘
src └─────────────┘
typ └─────────────┘
432 mul_inv_cancel := rat.mul_inv_cancel,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
433 inv_mul_cancel := rat.inv_mul_cancel,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
434 has_decidable_eq := rat.decidable_eq,
id └──────────────┘
src └──────────────┘
typ └──────────────┘
435 inv_zero := rfl }
id └─┘
src └─┘
typ └─┘
436
437 /- Extra instances to short-circuit type class resolution -/
438 instance : field ℚ := by apply_instance
id └───┘ ┴
src └───┘ ┴ └─────────────┘
typ └───┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
439 instance : division_ring ℚ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
440 instance : integral_domain ℚ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └──────────────
typ └─────────────┘ ┴ └──────────────
doc ┴ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
441 -- TODO(Mario): this instance slows down data.real.basic
src ─────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────
442 --instance : domain ℚ := by apply_instance
src ────────────────────────────────────────────────────┘
typ ────────────────────────────────────────────────────┘
doc ────────────────────────────────────────────────────┘
txt ────────────────────────────────────────────────────┘
par ────────────────────────────────────────────────────┘
pid ────────────────────────────────────────────────────┘
st ────────────────────────────────────────────────────┘
443 instance : nonzero_comm_ring ℚ := by apply_instance
id └───────────────┘ ┴
src └───────────────┘ ┴ └─────────────┘
typ └───────────────┘ ┴ └─────────────┘
doc └───────────────┘ ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
444 instance : comm_ring ℚ := by apply_instance
id └───────┘ ┴
src └───────┘ ┴ └──────────────
typ └───────┘ ┴ └──────────────
doc ┴ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
445 --instance : ring ℚ := by apply_instance
src ────────────────────────────────────────────────────┘
typ ────────────────────────────────────────────────────┘
doc ────────────────────────────────────────────────────┘
txt ────────────────────────────────────────────────────┘
par ────────────────────────────────────────────────────┘
pid ────────────────────────────────────────────────────┘
st ────────────────────────────────────────────────────┘
446 instance : comm_semiring ℚ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
447 instance : semiring ℚ := by apply_instance
id └──────┘ ┴
src └──────┘ ┴ └─────────────┘
typ └──────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
448 instance : add_comm_group ℚ := by apply_instance
id └────────────┘ ┴
src └────────────┘ ┴ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
449 instance : add_group ℚ := by apply_instance
id └───────┘ ┴
src └───────┘ ┴ └─────────────┘
typ └───────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
450 instance : add_comm_monoid ℚ := by apply_instance
id └─────────────┘ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
451 instance : add_monoid ℚ := by apply_instance
id └────────┘ ┴
src └────────┘ ┴ └─────────────┘
typ └────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
452 instance : add_left_cancel_semigroup ℚ := by apply_instance
id └───────────────────────┘ ┴
src └───────────────────────┘ ┴ └─────────────┘
typ └───────────────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
453 instance : add_right_cancel_semigroup ℚ := by apply_instance
id └────────────────────────┘ ┴
src └────────────────────────┘ ┴ └─────────────┘
typ └────────────────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
454 instance : add_comm_semigroup ℚ := by apply_instance
id └────────────────┘ ┴
src └────────────────┘ ┴ └─────────────┘
typ └────────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
455 instance : add_semigroup ℚ := by apply_instance
id └───────────┘ ┴
src └───────────┘ ┴ └─────────────┘
typ └───────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
456 instance : comm_monoid ℚ := by apply_instance
id └─────────┘ ┴
src └─────────┘ ┴ └─────────────┘
typ └─────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
457 instance : monoid ℚ := by apply_instance
id └────┘ ┴
src └────┘ ┴ └─────────────┘
typ └────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
458 instance : comm_semigroup ℚ := by apply_instance
id └────────────┘ ┴
src └────────────┘ ┴ └─────────────┘
typ └────────────┘ ┴ └─────────────┘
doc ┴ └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
459 instance : semigroup ℚ := by apply_instance
id └───────┘ ┴
src └───────┘ ┴ └──────────────
typ └───────┘ ┴ └──────────────
doc ┴ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
460
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
461 theorem sub_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
462 a /. b - c /. d = (a * d - c * b) /. (b * d) :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
463 by simp [b0, d0]
id └┘ └┘
src └────┘ └┘ └─
typ └────┘└┘└┘└┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────
464
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
465 @[simp] lemma denom_neg_eq_denom : ∀ q : ℚ, (-q).denom = q.denom
id ┴ ┴ ┴┴ └───┘ ┴ ┴└────┘
src ┴ ┴ └───┘ ┴ └────┘
typ ┴ ┴ ┴┴ └───┘ ┴ ┴└────┘
doc └──┘ ┴
466 | ⟨_, d, _, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
467
468 @[simp] lemma num_neg_eq_neg_num : ∀ q : ℚ, (-q).num = -(q.num)
id ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴└──┘
src ┴ ┴ └─┘ ┴ ┴ └──┘
typ ┴ ┴ ┴┴ └─┘ ┴ ┴ ┴└──┘
doc └──┘ ┴
469 | ⟨n, _, _, _⟩ := rfl
id └─┘
src └─┘
typ └─┘
470
471 @[simp] lemma num_zero : rat.num 0 = 0 := rfl
id └─────┘ ┴ └─┘
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘
doc └──┘
472
473 lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0 :=
id ┴ ┴└──┘ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ ┴└──┘ ┴ ┴ ┴
doc ┴
474 have q = q.num /. q.denom, from num_denom.symm,
id ┴ ┴ ┴└──┘ └┘ ┴└────┘ └───────┘└───┘
src ┴ └──┘ └┘ └────┘ └───────┘└───┘
typ ┴ ┴ ┴└──┘ └┘ ┴└────┘ └───────┘└───┘
doc └┘
475 by simpa [hq]
id └┘
src └─────┘ └─
typ └─────┘└┘└─
doc └─────┘ └─
txt └─────┘ └─
par └─────┘ └─
pid ┴┴ ┴└
st └───────────
476
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
477 lemma zero_iff_num_zero {q : ℚ} : q = 0 ↔ q.num = 0 :=
id ┴ ┴ ┴ ┴ ┴└──┘ ┴
src ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴└──┘ ┴
doc ┴
478 ⟨λ _, by simp *, zero_of_num_zero⟩
id ┴ └──────────────┘
src └────┘ └──────────────┘
typ ┴ └────┘ └──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴┴
st └─────┘
479
480 lemma num_ne_zero_of_ne_zero {q : ℚ} (h : q ≠ 0) : q.num ≠ 0 :=
id ┴ ┴ ┴ ┴└──┘ ┴
src ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴└──┘ ┴
doc ┴
481 assume : q.num = 0,
id ┴└──┘ ┴
src └──┘ ┴
typ ┴└──┘ ┴
482 h $ zero_of_num_zero this
id ┴ └──────────────┘ └──┘
src └──────────────┘
typ ┴ └──────────────┘ └──┘
483
484 @[simp] lemma num_one : (1 : ℚ).num = 1 := rfl
id ┴ └─┘ ┴ └─┘
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ └─┘
doc └──┘ ┴
485
486 @[simp] lemma denom_one : (1 : ℚ).denom = 1 := rfl
id ┴ └───┘ ┴ └─┘
src ┴ └───┘ ┴ └─┘
typ ┴ └───┘ ┴ └─┘
doc └──┘ ┴
487
488 lemma denom_ne_zero (q : ℚ) : q.denom ≠ 0 :=
id ┴ ┴└────┘ ┴
src ┴ └────┘ ┴
typ ┴ ┴└────┘ ┴
doc ┴
489 ne_of_gt q.pos
id └──────┘ ┴└──┘
src └──────┘ └──┘
typ └──────┘ ┴└──┘
490
491 lemma eq_iff_mul_eq_mul {p q : ℚ} : p = q ↔ p.num * q.denom = q.num * p.denom :=
id ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└────┘ ┴ ┴└──┘ ┴ ┴└────┘
src ┴ ┴ ┴ └──┘ ┴ └────┘ ┴ └──┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└────┘ ┴ ┴└──┘ ┴ ┴└────┘
doc ┴
492 begin
st └─────
493 conv_lhs { rw [←(@num_denom p), ←(@num_denom q)] },
id └───────┘ ┴ └───────┘ ┴
src └─────────┘└───┘ └───────┘┴ └──┘ └───────┘┴ └─┘┴
typ └─────────┘└───┘ └───────┘┴┴└──┘ └───────┘┴┴└─┘┴
txt └─────────┘└───┘ ┴ └──┘ ┴ └─┘┴
par └─────────┘└───┘ ┴ └──┘ ┴ └─┘┴
pid ┴└─────┘ ┴ └──┘ ┴ └──┘
st ───────────┘└──────────────────┘└───────────────┘ ┴└┘└
494 exact rat.mk_eq (by exact_mod_cast p.denom_ne_zero) (by exact_mod_cast q.denom_ne_zero)
id └───────┘ └─────────────┘ └─────────────┘
src └────┘└───────┘┴ ┴└─────────────┘└─────────────┘└┘ ┴└─────────────┘└─────────────┘└┘
typ └────┘└───────┘┴ └──────────────┘└─────────────┘└┘ └──────────────┘└─────────────┘└┘
doc └────┘ ┴ ┴└─────────────┘ └┘ ┴└─────────────┘ └┘
txt └────┘ ┴ ┴└─────────────┘ └┘ ┴└─────────────┘ └┘
par └────┘ ┴ └──────────────┘ └┘ └──────────────┘ └┘
pid ┴ ┴ └──────────────┘ └┘ └──────────────┘ ┴┴
st ────────────────────┘└─────────────────────────────┘└───┘└─────────────────────────────┘└┘
495 end
st └─┘
496
497 lemma mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc ┴ └┘
498 assume : n = 0,
id ┴ ┴
src ┴
typ ┴ ┴
499 hq $ by simpa [this] using hqnd
id └┘ └──┘ └──┘
src └─────┘ └──────┘ └
typ └┘ └─────┘└──┘└──────┘└──┘└
doc └─────┘ └──────┘ └
txt └─────┘ └──────┘ └
par └─────┘ └──────┘ └
pid ┴┴ ┴┴└────┘ └
st └────────────────────────
500
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
501 lemma mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : d ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc ┴ └┘
502 assume : d = 0,
id ┴ ┴
src ┴
typ ┴ ┴
503 hq $ by simpa [this] using hqnd
id └┘ └──┘ └──┘
src └─────┘ └──────┘ └
typ └┘ └─────┘└──┘└──────┘└──┘└
doc └─────┘ └──────┘ └
txt └─────┘ └──────┘ └
par └─────┘ └──────┘ └
pid ┴┴ ┴┴└────┘ └
st └────────────────────────
504
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
505 lemma mk_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) : n /. d ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘
506 assume : n /. d = 0,
id ┴ └┘ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴
doc └┘
507 h $ (mk_eq_zero hd).1 this
id ┴ └────────┘ └┘ ┴ └──┘
src └────────┘ ┴
typ ┴ └────────┘ └┘ ┴ └──┘
508
509 lemma mul_num_denom (q r : ℚ) : q * r = (q.num * r.num) /. ↑(q.denom * r.denom) :=
id ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ └┘ ┴ ┴└────┘ ┴ ┴└────┘
src ┴ ┴ ┴ └──┘ ┴ └──┘ └┘ ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ └┘ ┴ ┴└────┘ ┴ ┴└────┘
doc ┴ └┘
510 have hq' : (↑q.denom : ℤ) ≠ 0, by have := denom_ne_zero q; simpa,
id ┴┴└────┘ ┴ ┴ └───────────┘ ┴
src ┴ └────┘ ┴ ┴ └──────┘└───────────┘┴ └───┘
typ ┴┴└────┘ ┴ ┴ └──────┘└───────────┘┴┴ └───┘
doc └──────┘ ┴ └───┘
txt └──────┘ ┴ └───┘
par └──────┘ ┴ └───┘
pid └───┘└─┘ ┴
st └─────────────────────────────┘
511 have hr' : (↑r.denom : ℤ) ≠ 0, by have := denom_ne_zero r; simpa,
id ┴┴└────┘ ┴ ┴ └───────────┘ ┴
src ┴ └────┘ ┴ ┴ └──────┘└───────────┘┴ └───┘
typ ┴┴└────┘ ┴ ┴ └──────┘└───────────┘┴┴ └───┘
doc └──────┘ ┴ └───┘
txt └──────┘ ┴ └───┘
par └──────┘ ┴ └───┘
pid └───┘└─┘ ┴
st └─────────────────────────────┘
512 suffices (q.num /. ↑q.denom) * (r.num /. ↑r.denom) = (q.num * r.num) /. ↑(q.denom * r.denom),
id ┴└──┘ └┘ ┴┴└────┘ ┴ ┴└──┘ └┘ ┴┴└────┘ ┴ ┴└──┘ ┴ ┴└──┘ └┘ ┴ ┴└────┘ ┴ ┴└────┘
src └──┘ └┘ ┴ └────┘ ┴ └──┘ └┘ ┴ └────┘ ┴ └──┘ ┴ └──┘ └┘ ┴ └────┘ ┴ └────┘
typ ┴└──┘ └┘ ┴┴└────┘ ┴ ┴└──┘ └┘ ┴┴└────┘ ┴ ┴└──┘ ┴ ┴└──┘ └┘ ┴ ┴└────┘ ┴ ┴└────┘
doc └┘ └┘ └┘
513 by simpa using this,
id └──┘
src └──────────┘
typ └──────────┘└──┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └───────────────┘
514 by simp [mul_def hq' hr', -num_denom]
id └─────┘ └─┘ └─┘
src └────┘└─────┘┴ ┴ └─────────────
typ └────┘└─────┘┴└─┘┴└─┘└─────────────
doc └────┘ ┴ ┴ └─────────────
txt └────┘ ┴ ┴ └─────────────
par └────┘ ┴ ┴ └─────────────
pid ┴┴ ┴ ┴ └───────────┘└
st └───────────────────────────────────
515
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
516 lemma div_num_denom (q r : ℚ) : q / r = (q.num * r.denom) /. (q.denom * r.num) :=
id ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└────┘ └┘ ┴└────┘ ┴ ┴└──┘
src ┴ ┴ ┴ └──┘ ┴ └────┘ └┘ └────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└────┘ └┘ ┴└────┘ ┴ ┴└──┘
doc ┴ └┘
517 if hr : r.num = 0 then
id └┘ ┴└──┘ ┴
src └┘ └──┘ ┴
typ └┘ ┴└──┘ ┴
518 have hr' : r = 0, from zero_of_num_zero hr,
id ┴ ┴ └──────────────┘ └┘
src ┴ └──────────────┘
typ ┴ ┴ └──────────────┘ └┘
519 by simp *
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴┴┴
st └──────┘
520 else calc q / r = q * r⁻¹ : div_eq_mul_inv
id ┴ ┴ ┴ ┴ ┴ ┴└┘ └────────────┘
src ┴ ┴ └┘ └────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴└┘ └────────────┘
521 ... = (q.num /. q.denom) * (r.num /. r.denom)⁻¹ : by simp
id ┴└──┘ └┘ ┴└────┘ ┴ ┴└──┘ └┘ ┴└────┘ └┘
src └──┘ └┘ └────┘ ┴ └──┘ └┘ └────┘ └┘ └────
typ ┴└──┘ └┘ ┴└────┘ ┴ ┴└──┘ └┘ ┴└────┘ └┘ └────
doc └┘ └┘ └────
txt └────
par └────
pid └
st └─────
522 ... = (q.num /. q.denom) * (r.denom /. r.num) : by rw inv_def
id ┴└──┘ └┘ ┴└────┘ ┴ ┴└────┘ └┘ ┴└──┘ └─────┘
src ───────────┘ └──┘ └┘ └────┘ ┴ └────┘ └┘ └──┘ └─┘└─────┘└
typ ───────────┘ ┴└──┘ └┘ ┴└────┘ ┴ ┴└────┘ └┘ ┴└──┘ └─┘└─────┘└
doc ───────────┘ └┘ └┘ └─┘ └
txt ───────────┘ └─┘ └
par ───────────┘ └─┘ └
pid ───────────┘ ┴ └
st ───────────┘ └───────────
523 ... = (q.num * r.denom) /. (q.denom * r.num) : mul_def (by simpa using denom_ne_zero q) hr
id └─┘ ┴└──┘ ┴ ┴└────┘ └┘ ┴└────┘ ┴ ┴└──┘ └─────┘ └───────────┘ ┴ └┘
src ───────────┘ └──┘ ┴ └────┘ └┘ └────┘ ┴ └──┘ └─────┘ └──────────┘└───────────┘┴
typ ───────────┘└─┘ ┴└──┘ ┴ ┴└────┘ └┘ ┴└────┘ ┴ ┴└──┘ └─────┘ └──────────┘└───────────┘┴┴ └┘
doc ───────────┘ └┘ └──────────┘ ┴
txt ───────────┘ └──────────┘ ┴
par ───────────┘ └──────────┘ ┴
pid ───────────┘ ┴└────┘ ┴
st ───────────┘ └──────────────────────────┘
524
525 lemma num_denom_mk {q : ℚ} {n d : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (qdf : q = n /. d) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
526 ∃ c : ℤ, n = c * q.num ∧ d = c * q.denom :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘
src ┴ ┴┴ ┴ ┴ └──┘ ┴ ┴ ┴ └────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘
527 have hq : q ≠ 0, from
id ┴ ┴
src ┴
typ ┴ ┴
528 assume : q = 0,
id ┴ ┴
src ┴
typ ┴ ┴
529 hn $ (rat.mk_eq_zero hd).1 (by cc),
id └┘ └────────────┘ └┘ ┴
src └────────────┘ ┴ └┘
typ └┘ └────────────┘ └┘ ┴ └┘
doc └┘
txt └┘
par └┘
st └─┘
530 have q.num /. q.denom = n /. d, by rwa [num_denom],
id ┴└──┘ └┘ ┴└────┘ ┴ ┴ └┘ ┴ └───────┘
src └──┘ └┘ └────┘ ┴ └┘ └───┘└───────┘┴
typ ┴└──┘ └┘ ┴└────┘ ┴ ┴ └┘ ┴ └───┘└───────┘┴
doc └┘ └┘ └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └─────────────┘┴
531 have q.num * d = n * ↑(q.denom), from (rat.mk_eq (by simp [rat.denom_ne_zero]) hd).1 this,
id ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘ └───────┘ └───────────────┘ └┘ ┴ └──┘
src └──┘ ┴ ┴ ┴ ┴ └────┘ └───────┘ └────┘└───────────────┘┴ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘ └───────┘ └────┘└───────────────┘┴ └┘ ┴ └──┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────────┘
532 begin
st └─────
533 existsi n / q.num,
id ┴ ┴ └───┘
src └──────┘ ┴┴┴└───┘
typ └──────┘┴┴┴┴└───┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────┘└─
534 have hqdn : q.num ∣ n, begin rw qdf, apply rat.num_dvd, assumption end,
id └───┘ ┴ ┴ └─┘ └─────────┘
src └──────────┘└───┘┴┴┴ └─┘ └────┘└─────────┘ └─────────┘
typ └──────────┘└───┘┴┴┴┴ └─┘└─┘ └────┘└─────────┘ └─────────┘
doc └──────────┘ ┴ ┴ └─┘ └────┘ └─────────┘
txt └──────────┘ ┴ ┴ └─┘ └────┘ └─────────┘
par └──────────┘ ┴ ┴ └─┘ └────┘ └─────────┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────┘└─────┘└─────┘└─────────────────┘└───────────┘└─┘└─
535 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
536 { rw int.div_mul_cancel hqdn },
id └────────────────┘ └──┘
src └─┘└────────────────┘┴ ┴
typ └─┘└────────────────┘┴└──┘┴
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└─────────────────────────┘└┘└
537 { apply int.eq_mul_div_of_mul_eq_mul_of_dvd_left,
id └──────────────────────────────────────┘
src └────┘└──────────────────────────────────────┘
typ └────┘└──────────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────────────────────────┘└─
538 {apply rat.num_ne_zero_of_ne_zero hq},
id └────────────────────────┘ └┘
src └────┘└────────────────────────┘┴
typ └────┘└────────────────────────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────────┘└┘└
539 {simp [rat.denom_ne_zero]},
id └───────────────┘
src └────┘└───────────────┘┴
typ └────┘└───────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────────────────┘└┘└
540 repeat {assumption} }
src └──────┘└────────┘└┘
typ └──────┘└────────┘└┘
doc └──────┘└────────┘└┘
txt └──────┘└────────┘└┘
par └──────┘└────────┘└┘
pid └───────────┘┴
st ─────────────┘└────────┘┴┴└─
541 end
st ──┘
542
543 theorem mk_pnat_num (n : ℤ) (d : ℕ+) :
id ┴ └┘
src ┴ └┘
typ ┴ └┘
doc └┘
544 (mk_pnat n d).num = n / nat.gcd n.nat_abs d :=
id └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴└──────┘ ┴
src └─────┘ └─┘ ┴ ┴ └─────┘ └──────┘
typ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴└──────┘ ┴
doc └─────┘
545 by cases d; refl
id ┴
src └────┘ └────
typ └────┘┴ └────
doc └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └
st └──────────────
546
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
547 theorem mk_pnat_denom (n : ℤ) (d : ℕ+) :
id ┴ └┘
src ┴ └┘
typ ┴ └┘
doc └┘
548 (mk_pnat n d).denom = d / nat.gcd n.nat_abs d :=
id └─────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └─────┘ ┴└──────┘ ┴
src └─────┘ └───┘ ┴ ┴ └─────┘ └──────┘
typ └─────┘ ┴ ┴ └───┘ ┴ ┴ ┴ └─────┘ ┴└──────┘ ┴
doc └─────┘
549 by cases d; refl
id ┴
src └────┘ └────
typ └────┘┴ └────
doc └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └
st └──────────────
550
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
551 theorem mul_num (q₁ q₂ : ℚ) : (q₁ * q₂).num =
id ┴ └┘ ┴ └┘ └─┘ ┴
src ┴ ┴ └─┘ ┴
typ ┴ └┘ ┴ └┘ └─┘ ┴
doc ┴
552 (q₁.num * q₂.num) / nat.gcd (q₁.num * q₂.num).nat_abs (q₁.denom * q₂.denom) :=
id └┘└──┘ ┴ └┘└──┘ ┴ └─────┘ └┘└──┘ ┴ └┘└──┘ └─────┘ └┘└────┘ ┴ └┘└────┘
src └──┘ ┴ └──┘ ┴ └─────┘ └──┘ ┴ └──┘ └─────┘ └────┘ ┴ └────┘
typ └┘└──┘ ┴ └┘└──┘ ┴ └─────┘ └┘└──┘ ┴ └┘└──┘ └─────┘ └┘└────┘ ┴ └┘└────┘
553 by cases q₁; cases q₂; refl
id └┘ └┘
src └────┘ └────┘ └────
typ └────┘└┘ └────┘└┘ └────
doc └────┘ └────┘ └────
txt └────┘ └────┘ └────
par └────┘ └────┘ └────
pid ┴ ┴ └
st └─────────────────────────
554
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
555 theorem mul_denom (q₁ q₂ : ℚ) : (q₁ * q₂).denom =
id ┴ └┘ ┴ └┘ └───┘ ┴
src ┴ ┴ └───┘ ┴
typ ┴ └┘ ┴ └┘ └───┘ ┴
doc ┴
556 (q₁.denom * q₂.denom) / nat.gcd (q₁.num * q₂.num).nat_abs (q₁.denom * q₂.denom) :=
id └┘└────┘ ┴ └┘└────┘ ┴ └─────┘ └┘└──┘ ┴ └┘└──┘ └─────┘ └┘└────┘ ┴ └┘└────┘
src └────┘ ┴ └────┘ ┴ └─────┘ └──┘ ┴ └──┘ └─────┘ └────┘ ┴ └────┘
typ └┘└────┘ ┴ └┘└────┘ ┴ └─────┘ └┘└──┘ ┴ └┘└──┘ └─────┘ └┘└────┘ ┴ └┘└────┘
557 by cases q₁; cases q₂; refl
id └┘ └┘
src └────┘ └────┘ └────
typ └────┘└┘ └────┘└┘ └────
doc └────┘ └────┘ └────
txt └────┘ └────┘ └────
par └────┘ └────┘ └────
pid ┴ ┴ └
st └─────────────────────────
558
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
559 theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num :=
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘
src ┴ ┴ └─┘ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘
doc ┴
560 by rw [mul_num, int.nat_abs_mul, nat.coprime.gcd_eq_one, int.coe_nat_one, int.div_one];
id └─────┘ └─────────────┘ └────────────────────┘ └─────────────┘ └─────────┘
src └──┘└─────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────────┘└┘└─────────┘┴
typ └──┘└─────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────────┘└┘└─────────┘┴
doc └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st └──────────┘└───────────────┘└──────────────────────┘└───────────────┘└───────────┘┴└─
561 exact (q.cop.mul_right q.cop).mul (q.cop.mul_right q.cop)
id └─────────────┘ └───┘
src └────┘ ┴ └────┘ └─────────────┘┴└───┘└─
typ └────┘ ┴ └────┘ └─────────────┘┴└───┘└─
doc └────┘ ┴ └────┘ ┴ └─
txt └────┘ ┴ └────┘ ┴ └─
par └────┘ ┴ └────┘ ┴ └─
pid ┴ ┴ └────┘ ┴ ┴└
st ──────────────────────────────────────────────────────────
562
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
563 theorem mul_self_denom (q : ℚ) : (q * q).denom = q.denom * q.denom :=
id ┴ ┴ ┴ ┴ └───┘ ┴ ┴└────┘ ┴ ┴└────┘
src ┴ ┴ └───┘ ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ └───┘ ┴ ┴└────┘ ┴ ┴└────┘
doc ┴
564 by rw [rat.mul_denom, int.nat_abs_mul, nat.coprime.gcd_eq_one, nat.div_one];
id └───────────┘ └─────────────┘ └────────────────────┘ └─────────┘
src └──┘└───────────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────┘┴
typ └──┘└───────────┘└┘└─────────────┘└┘└────────────────────┘└┘└─────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └────────────────┘└───────────────┘└──────────────────────┘└───────────┘┴└─
565 exact (q.cop.mul_right q.cop).mul (q.cop.mul_right q.cop)
id └─────────────┘ └───┘
src └────┘ ┴ └────┘ └─────────────┘┴└───┘└─
typ └────┘ ┴ └────┘ └─────────────┘┴└───┘└─
doc └────┘ ┴ └────┘ ┴ └─
txt └────┘ ┴ └────┘ ┴ └─
par └────┘ ┴ └────┘ ┴ └─
pid ┴ ┴ └────┘ ┴ ┴└
st ──────────────────────────────────────────────────────────
566
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
567 lemma add_num_denom (q r : ℚ) : q + r =
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴
568 ((q.num * r.denom + q.denom * r.num : ℤ)) /. (↑q.denom * ↑r.denom : ℤ) :=
id ┴└──┘ ┴ ┴└────┘ ┴ ┴└────┘ ┴ ┴└──┘ ┴ └┘ ┴┴└────┘ ┴ ┴┴└────┘ ┴
src └──┘ ┴ └────┘ ┴ └────┘ ┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ └────┘ ┴
typ ┴└──┘ ┴ ┴└────┘ ┴ ┴└────┘ ┴ ┴└──┘ ┴ └┘ ┴┴└────┘ ┴ ┴┴└────┘ ┴
doc └┘
569 have hqd : (q.denom : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 q.3,
id ┴└────┘ ┴ ┴ └─────────────────────────┘┴ ┴┴
src └────┘ ┴ ┴ └─────────────────────────┘┴ ┴
typ ┴└────┘ ┴ ┴ └─────────────────────────┘┴ ┴┴
570 have hrd : (r.denom : ℤ) ≠ 0, from int.coe_nat_ne_zero_iff_pos.2 r.3,
id ┴└────┘ ┴ ┴ └─────────────────────────┘┴ ┴┴
src └────┘ ┴ ┴ └─────────────────────────┘┴ ┴
typ ┴└────┘ ┴ ┴ └─────────────────────────┘┴ ┴┴
571 by conv_lhs { rw [←@num_denom q, ←@num_denom r, rat.add_def hqd hrd] };
id └───────┘ ┴ └───────┘ ┴ └─────────┘ └─┘ └─┘
src └─────────┘└───┘ └───────┘┴ └─┘ └───────┘┴ └┘└─────────┘┴ ┴ └┘┴
typ └─────────┘└───┘ └───────┘┴┴└─┘ └───────┘┴┴└┘└─────────┘┴└─┘┴└─┘└┘┴
txt └─────────┘└───┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘┴
par └─────────┘└───┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘┴
pid ┴└─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘
st └─────────┘└────────────────┘└─────────────┘└───────────────────┘ ┴└┘└
572 simp [mul_comm]
id └──────┘
src └────┘└──────┘└─
typ └────┘└──────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ──────────────────
573
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
574 section casts
575
576 theorem coe_int_eq_mk : ∀ (z : ℤ), ↑z = z /. 1
id ┴ ┴ ┴┴ ┴ ┴ └┘
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴┴ ┴ ┴ └┘
doc └┘
577 | (n : ℕ) := show (n:ℚ) = n /. 1,
id ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
doc ┴ └┘
578 by induction n with n IH n; simp [*, show (1:ℚ) = 1 /. 1, from rfl]
id ┴ ┴ └─┘
src └────────┘ └──────────┘ └───────┘ ┴ └┘ └┘┴└─┘ └───────┘└─┘└┘
typ └────────┘┴└──────────┘ └───────┘ ┴ └┘ └┘┴└─┘ └───────┘└─┘└┘
doc └────────┘ └──────────┘ └───────┘ ┴ └┘ └┘ └─┘ └───────┘ └┘
txt └────────┘ └──────────┘ └───────┘ ┴ └┘ └┘ └─┘ └───────┘ └┘
par └────────┘ └──────────┘ └───────┘ ┴ └┘ └┘ └─┘ └───────┘ └┘
pid ┴ ┴└─────────┘ ┴└──┘ ┴ └┘ └┘ └─┘ └───────┘ ┴┴
st └────────────────────────────────────────────────────────────────┘
579 | -[1+ n] := show (-(n + 1) : ℚ) = -[1+ n] /. 1, begin
id └──┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
src └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
typ └──┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
doc ┴ └┘
st └─────
580 induction n with n IH, {refl},
id ┴
src └────────┘ └────────┘ └──┘
typ └────────┘┴└────────┘ └──┘
doc └────────┘ └────────┘ └──┘
txt └────────┘ └────────┘ └──┘
par └────────┘ └────────┘ └──┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─────┘└┘└
581 show -(n + 1 + 1 : ℚ) = -[1+ n.succ] /. 1,
id ┴ ┴ └────┘
src └───┘┴ ┴┴└─┘ └───┘ └┘ ┴ ┴└────┘ ┴ └┘
typ └───┘┴ ┴┴└─┘ └───┘ └┘ ┴ ┴└────┘ ┴ └┘
doc └───┘ ┴ └─┘ └───┘ └┘ ┴ ┴ ┴ └┘
txt └───┘ ┴ └─┘ └───┘ └┘ ┴ ┴ ┴ └┘
par └───┘ ┴ └─┘ └───┘ └┘ ┴ ┴ ┴ └┘
pid └───┘ ┴ └─┘ └───┘ └┘ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────┘└─
582 rw [neg_add, IH],
id └─────┘ └┘
src └──┘└─────┘└┘ ┴
typ └──┘└─────┘└┘└┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────┘└──┘└──
583 simpa [show -1 = (-1) /. 1, from rfl]
id ┴ └─┘
src └─────┘ ┴ └┘ ┴ └─┘ └───────┘└─┘└┘
typ └─────┘ ┴ └┘┴┴ └─┘ └───────┘└─┘└┘
doc └─────┘ ┴ └┘ ┴ └─┘ └───────┘ └┘
txt └─────┘ ┴ └┘ ┴ └─┘ └───────┘ └┘
par └─────┘ ┴ └┘ ┴ └─┘ └───────┘ └┘
pid ┴┴ ┴ └┘ ┴ └─┘ └───────┘ ┴┴
st ───────────────────────────────────────┘
584 end
st └─┘
585
586 theorem mk_eq_div (n d : ℤ) : n /. d = ((n : ℚ) / d) :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ ┴
587 begin
st └─────
588 by_cases d0 : d = 0, {simp [d0, div_zero]},
id ┴ ┴ └┘ └──────┘
src └───────┘ └─┘ ┴┴└┘ └────┘ └┘└──────┘┴
typ └───────┘ └─┘┴┴┴└┘ └────┘└┘└┘└──────┘┴
doc └───────┘ └─┘ ┴ └┘ └────┘ └┘ ┴
txt └───────┘ └─┘ ┴ └┘ └────┘ └┘ ┴
par └───────┘ └─┘ ┴ └┘ └────┘ └┘ ┴
pid ┴ └─┘ ┴ ┴┴ ┴┴ └┘ ┴
st ────────────────────┘└────────────────────┘└┘└
589 simp [division_def, coe_int_eq_mk, mul_def one_ne_zero d0]
id └──────────┘ └───────────┘ └─────┘ └─────────┘ └┘
src └────┘└──────────┘└┘└───────────┘└┘└─────┘┴└─────────┘┴ └┘
typ └────┘└──────────┘└┘└───────────┘└┘└─────┘┴└─────────┘┴└┘└┘
doc └────┘ └┘ └┘ ┴ ┴ └┘
txt └────┘ └┘ └┘ ┴ ┴ └┘
par └────┘ └┘ └┘ ┴ ┴ └┘
pid ┴┴ └┘ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────┘
590 end
st └─┘
591
592 theorem coe_int_eq_of_int (z : ℤ) : ↑z = of_int z :=
id ┴ ┴┴ ┴ └────┘ ┴
src ┴ ┴ ┴ └────┘
typ ┴ ┴┴ ┴ └────┘ ┴
doc └────┘
593 (coe_int_eq_mk z).trans (of_int_eq_mk z).symm
id └───────────┘ ┴ └───┘ └──────────┘ ┴ └──┘
src └───────────┘ └───┘ └──────────┘ └──┘
typ └───────────┘ ┴ └───┘ └──────────┘ ┴ └──┘
594
595 @[simp, elim_cast] theorem coe_int_num (n : ℤ) : (n : ℚ).num = n :=
id ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └───────┘ ┴
596 by rw coe_int_eq_of_int; refl
id └───────────────┘
src └─┘└───────────────┘ └────
typ └─┘└───────────────┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────────────
597
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
598 @[simp, elim_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1 :=
id ┴ ┴ ┴ └───┘ ┴
src ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ └───┘ ┴
doc └──┘ └───────┘ ┴
599 by rw coe_int_eq_of_int; refl
id └───────────────┘
src └─┘└───────────────┘ └────
typ └─┘└───────────────┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────────────
600
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
601 lemma coe_int_num_of_denom_eq_one {q : ℚ} (hq : q.denom = 1) : ↑(q.num) = q :=
id ┴ ┴└────┘ ┴ ┴ ┴└──┘ ┴ ┴
src ┴ └────┘ ┴ ┴ └──┘ ┴
typ ┴ ┴└────┘ ┴ ┴ ┴└──┘ ┴ ┴
doc ┴
602 by { conv_rhs { rw [←(@num_denom q), hq] }, rw [coe_int_eq_mk], refl }
id └───────┘ ┴ └┘ └───────────┘
src └─────────┘└───┘ └───────┘┴ └─┘ └┘┴ └──┘└───────────┘┴ └───┘
typ └─────────┘└───┘ └───────┘┴┴└─┘└┘└┘┴ └──┘└───────────┘┴ └───┘
doc └──┘ ┴ └───┘
txt └─────────┘└───┘ ┴ └─┘ └┘┴ └──┘ ┴ └───┘
par └─────────┘└───┘ ┴ └─┘ └┘┴ └──┘ ┴ └───┘
pid ┴└─────┘ ┴ └─┘ └─┘ └┘ ┴ ┴
st └───────────┘└──────────────────┘└──┘ ┴└┘└────────────────┘└──────┘└┘
603
604 instance : can_lift ℚ ℤ :=
id └──────┘ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴
doc └──────┘ ┴
605 ⟨coe, λ q, q.denom = 1, λ q hq, ⟨q.num, coe_int_num_of_denom_eq_one hq⟩⟩
id └─┘ ┴ ┴└────┘ ┴ ┴ └┘ ┴└──┘ └─────────────────────────┘ └┘
src └─┘ └────┘ ┴ └──┘ └─────────────────────────┘
typ └─┘ ┴ ┴└────┘ ┴ ┴ └┘ ┴└──┘ └─────────────────────────┘ └┘
606
607 theorem coe_nat_eq_mk (n : ℕ) : ↑n = n /. 1 :=
id ┴ ┴┴ ┴ ┴ └┘
src ┴ ┴ ┴ └┘
typ ┴ ┴┴ ┴ ┴ └┘
doc └┘
608 by rw [← int.cast_coe_nat, coe_int_eq_mk]
id └──────────────┘ └───────────┘
src └────┘└──────────────┘└┘└───────────┘└─
typ └────┘└──────────────┘└┘└───────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └─────────────────────┘└─────────────┘┴└
609
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
610 @[simp, elim_cast] theorem coe_nat_num (n : ℕ) : (n : ℚ).num = n :=
id ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └───────┘ ┴
611 by rw [← int.cast_coe_nat, coe_int_num]
id └──────────────┘ └─────────┘
src └────┘└──────────────┘└┘└─────────┘└─
typ └────┘└──────────────┘└┘└─────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └─────────────────────┘└───────────┘┴└
612
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
613 @[simp, elim_cast] theorem coe_nat_denom (n : ℕ) : (n : ℚ).denom = 1 :=
id ┴ ┴ ┴ └───┘ ┴
src ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ └───┘ ┴
doc └──┘ └───────┘ ┴
614 by rw [← int.cast_coe_nat, coe_int_denom]
id └──────────────┘ └───────────┘
src └────┘└──────────────┘└┘└───────────┘└─
typ └────┘└──────────────┘└┘└───────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ ┴└
st └─────────────────────┘└─────────────┘┴└
615
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
616 end casts
617
618 lemma inv_def' {q : ℚ} : q⁻¹ = (q.denom : ℚ) / q.num :=
id ┴ ┴└┘ ┴ ┴└────┘ ┴ ┴ ┴└──┘
src ┴ └┘ ┴ └────┘ ┴ ┴ └──┘
typ ┴ ┴└┘ ┴ ┴└────┘ ┴ ┴ ┴└──┘
doc ┴ ┴
619 by { conv_lhs { rw ←(@num_denom q) }, cases q, simp [div_num_denom] }
id └───────┘ ┴ ┴ └───────────┘
src └─────────┘└──┘ └───────┘┴ └┘┴ └────┘ └────┘└───────────┘└┘
typ └─────────┘└──┘ └───────┘┴┴└┘┴ └────┘┴ └────┘└───────────┘└┘
doc └────┘ └────┘ └┘
txt └─────────┘└──┘ ┴ └┘┴ └────┘ └────┘ └┘
par └─────────┘└──┘ ┴ └┘┴ └────┘ └────┘ └┘
pid ┴└────┘ ┴ └─┘ ┴ ┴┴ ┴┴
st └───────────┘└──────────────────┘└┘└──────┘└─────────────────────┘└┘
620
621 @[simp] lemma mul_own_denom_eq_num {q : ℚ} : q * q.denom = q.num :=
id ┴ ┴ ┴ ┴└────┘ ┴ ┴└──┘
src ┴ ┴ └────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴└────┘ ┴ ┴└──┘
doc └──┘ ┴
622 begin
st └─────
623 suffices : mk (q.num) ↑(q.denom) * mk ↑(q.denom) 1 = mk (q.num) 1, by
id ┴ ┴ └─────┘ ┴ └┘ └───┘
src └─────────┘ ┴ └┘┴ └┘┴┴ ┴ └─────┘└──┘┴┴└┘┴ └───┘└─┘
typ └─────────┘ ┴ └┘┴ └┘┴┴ ┴ └─────┘└──┘┴┴└┘┴ └───┘└─┘
doc └─────────┘ ┴ └┘ └┘ ┴ ┴ └──┘ ┴└┘┴ └─┘
txt └─────────┘ ┴ └┘ └┘ ┴ ┴ └──┘ ┴ ┴ └─┘
par └─────────┘ ┴ └┘ └┘ ┴ ┴ └──┘ ┴ ┴ └─┘
pid └───────┘└┘ ┴ └┘ └┘ ┴ ┴ └──┘ ┴ ┴ └┘┴
st ──────────────────────────────────────────────────────────────────┘
624 { conv { for q [1] { rw ←(@num_denom q) }}, rwa [coe_int_eq_mk, coe_nat_eq_mk] },
id ┴ └───────┘ ┴ └───────────┘ └───────────┘
src └─────┘└──┘ └─────┘└──┘ └───────┘┴ └┘┴┴ └───┘└───────────┘└┘└───────────┘└┘
typ └─────┘└──┘┴└─────┘└──┘ └───────┘┴┴└┘┴┴ └───┘└───────────┘└┘└───────────┘└┘
doc └───┘ └┘ └┘
txt └─────┘└──┘ └─────┘└──┘ ┴ └┘┴┴ └───┘ └┘ └┘
par └─────┘└──┘ └─────┘└──┘ ┴ └┘┴┴ └───┘ └┘ └┘
pid ┴└────┘ └─────────┘ ┴ └──┘ └┘ └┘ ┴┴
st ┴└─────┘└──────────┘└──────────────────┘└┘┴└─────────────────┘└─────────────┘┴┴└┘└
625 have : (q.denom : ℤ) ≠ 0, from ne_of_gt (by exact_mod_cast q.pos),
id └─────┘ ┴ └──────┘ └───┘
src └─────┘ └─────┘└─┘ └┘┴└┘ └───┘└──────┘┴ ┴└─────────────┘└───┘┴
typ └─────┘ └─────┘└─┘ └┘┴└┘ └───┘└──────┘┴ └──────────────┘└───┘┴
doc └─────┘ └─┘ └┘ └┘ └───┘ ┴ ┴└─────────────┘ ┴
txt └─────┘ └─┘ └┘ └┘ └───┘ ┴ ┴└─────────────┘ ┴
par └─────┘ └─┘ └┘ └┘ └───┘ ┴ └──────────────┘ ┴
pid └───┘└┘ └─┘ └┘ ┴┴ └───┘ ┴ └──────────────┘ ┴
st ─────────────────────────┘└─────────────────┘└───────────────────┘┴└─
626 rw [(rat.mul_def this one_ne_zero), (mul_comm (q.denom : ℤ) 1), (div_mk_div_cancel_left this)]
id └─────────┘ └──┘ └─────────┘ └──────┘ └─────┘ └────────────────────┘ └──┘
src └──┘ └─────────┘┴ ┴└─────────┘└─┘ └──────┘┴ └─────┘└─┘ └────┘ └────────────────────┘┴ └─┘
typ └──┘ └─────────┘┴└──┘┴└─────────┘└─┘ └──────┘┴ └─────┘└─┘ └────┘ └────────────────────┘┴└──┘└─┘
doc └──┘ ┴ ┴ └─┘ ┴ └─┘ └────┘ ┴ └─┘
txt └──┘ ┴ ┴ └─┘ ┴ └─┘ └────┘ ┴ └─┘
par └──┘ ┴ ┴ └─┘ ┴ └─┘ └────┘ ┴ └─┘
pid └┘ ┴ ┴ └─┘ ┴ └─┘ └────┘ ┴ └┘┴
st ───────────────────────────────────┘└──────────────────────────┘└─────────────────────────────┘┴┴
627 end
st └─┘
628
629 end rat